Theorem pweqi 4572

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

This proof depends on syntax axioms:   = wceq 1569  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-pw 4558

This theorem is used by:  rankxplim  9903  pwdju1  10276  fin23lem17  10423  mnfnre  11359  qtopres  24026  hmphdis  24124  ust0  24548  made0  28258  umgrpredgv  29727  lfuhgr  29735  issubgr  29861  uhgrissubgr  29865  cusgredg  30014  cffldtocusgr  30037  konigsbergiedgw  30858  shsspwh  31857  circtopn  34519  r11  35783  r12  35784  rankeq1o  37056  onsucsuccmpi  37355  bj-unirel  38102  elrfi  43842  islmodfg  44208  clsk1indlem4  45181  clsk1indlem1  45182  clsk1independent  45183  omef  47642  caragensplit  47646  caragenelss  47647  carageneld  47648  omeunile  47651  caragensspw  47655  0ome  47675  isomennd  47677  ovn02  47714  isuspgrimlem  49129  grtri  49174  usgrexmpl1lem  49255  usgrexmpl2lem  49260  lcoop  49659  lincvalsc0  49669  linc0scn0  49671  lincdifsn  49672  linc1  49673  lspsslco  49685  lincresunit3lem2  49728  lincresunit3  49729