Theorem pweqi 4559

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 4557	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	ax-mp 5	1 ⊢ 𝒫 𝐴 = 𝒫 𝐵

Syntax hints:   = wceq 1537  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  pwfi  8821  rankxplim  9310  pwdju1  9618  fin23lem17  9762  mnfnre  10686  qtopres  22308  hmphdis  22406  ust0  22830  umgrpredgv  26927  issubgr  27055  uhgrissubgr  27059  cusgredg  27208  cffldtocusgr  27231  konigsbergiedgw  28029  shsspwh  29025  circtopn  31103  lfuhgr  32366  rankeq1o  33634  onsucsuccmpi  33793  bj-unirel  34346  elrfi  39298  islmodfg  39676  clsk1indlem4  40401  clsk1indlem1  40402  clsk1independent  40403  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