Theorem pweqi 4560

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

Hypothesis

Ref	Expression
pweqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
pweqi	⊢ 𝒫 𝐴 = 𝒫 𝐵

Proof of Theorem pweqi

Step	Hyp	Ref	Expression
1		pweqi.1	. 2 ⊢ 𝐴 = 𝐵
2		pweq 4558	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	ax-mp 5	1 ⊢ 𝒫 𝐴 = 𝒫 𝐵

Syntax hints:   = wceq 1536  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-in 3946  df-ss 3955  df-pw 4544

This theorem is referenced by:  pwfi  8822  rankxplim  9311  pwdju1  9619  fin23lem17  9763  mnfnre  10687  qtopres  22309  hmphdis  22407  ust0  22831  umgrpredgv  26928  issubgr  27056  uhgrissubgr  27060  cusgredg  27209  cffldtocusgr  27232  konigsbergiedgw  28030  shsspwh  29026  circtopn  31105  lfuhgr  32368  rankeq1o  33636  onsucsuccmpi  33795  bj-unirel  34348  elrfi  39297  islmodfg  39675  clsk1indlem4  40400  clsk1indlem1  40401  clsk1independent  40402  omef  42785  caragensplit  42789  caragenelss  42790  carageneld  42791  omeunile  42794  caragensspw  42798  0ome  42818  isomennd  42820  ovn02  42857  lcoop  44473  lincvalsc0  44483  linc0scn0  44485  lincdifsn  44486  linc1  44487  lspsslco  44499  lincresunit3lem2  44542  lincresunit3  44543