Theorem pweqi 4302

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

Syntax hints:   = wceq 1631  𝒫 cpw 4298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3731  df-ss 3738  df-pw 4300

This theorem is referenced by:  pwfi  8418  rankxplim  8907  pwcda1  9219  fin23lem17  9363  mnfnre  10285  qtopres  21723  hmphdis  21821  ust0  22244  umgrpredgv  26258  issubgr  26387  uhgrissubgr  26391  cusgredg  26556  cffldtocusgr  26579  konigsbergiedgw  27429  shsspwh  28444  circtopn  30245  rankeq1o  32616  onsucsuccmpi  32780  elrfi  37784  islmodfg  38166  clsk1indlem4  38869  clsk1indlem1  38870  clsk1independent  38871  omef  41231  caragensplit  41235  caragenelss  41236  carageneld  41237  omeunile  41240  caragensspw  41244  0ome  41264  isomennd  41266  ovn02  41303  lcoop  42729  lincvalsc0  42739  linc0scn0  42741  lincdifsn  42742  linc1  42743  lspsslco  42755  lincresunit3lem2  42798  lincresunit3  42799