Theorem pweqi 4162

Description: Equality inference for power class. (Contributed by NM, 27-Nov-2013.)

Hypothesis

Ref	Expression
pweqi.1	|- A = B

Assertion

Ref	Expression
pweqi	|- ~P A = ~P B

Proof of Theorem pweqi

Step	Hyp	Ref	Expression
1		pweqi.1	. 2 |- A = B
2		pweq 4161	. 2 |- ( A = B -> ~P A = ~P B )
3	1, 2	ax-mp 5	1 |- ~P A = ~P B

Syntax hints:   = wceq 1483   ~Pcpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  pwfi  8261  rankxplim  8742  pwcda1  9016  fin23lem17  9160  mnfnre  10082  qtopres  21501  hmphdis  21599  ust0  22023  umgrpredgv  26035  issubgr  26163  uhgrissubgr  26167  cusgredg  26320  cffldtocusgr  26343  konigsbergiedgw  27108  konigsbergiedgwOLD  27109  shsspwh  28103  circtopn  29904  rankeq1o  32278  onsucsuccmpi  32442  elrfi  37257  islmodfg  37639  clsk1indlem4  38342  clsk1indlem1  38343  clsk1independent  38344  omef  40710  caragensplit  40714  caragenelss  40715  carageneld  40716  omeunile  40719  caragensspw  40723  0ome  40743  isomennd  40745  ovn02  40782  lcoop  42200  lincvalsc0  42210  linc0scn0  42212  lincdifsn  42213  linc1  42214  lspsslco  42226  lincresunit3lem2  42269  lincresunit3  42270