Theorem pweqi 4558

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

Syntax hints:   = wceq 1542  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  rankxplim  9797  pwdju1  10107  fin23lem17  10254  mnfnre  11182  qtopres  23676  hmphdis  23774  ust0  24198  made0  27872  umgrpredgv  29226  issubgr  29357  uhgrissubgr  29361  cusgredg  29510  cffldtocusgr  29533  cffldtocusgrOLD  29534  konigsbergiedgw  30336  shsspwh  31335  circtopn  34000  r11  35256  r12  35257  lfuhgr  35319  rankeq1o  36372  onsucsuccmpi  36644  bj-unirel  37377  elrfi  43143  islmodfg  43518  clsk1indlem4  44492  clsk1indlem1  44493  clsk1independent  44494  omef  46945  caragensplit  46949  caragenelss  46950  carageneld  46951  omeunile  46954  caragensspw  46958  0ome  46978  isomennd  46980  ovn02  47017  isuspgrimlem  48386  grtri  48431  usgrexmpl1lem  48512  usgrexmpl2lem  48517  lcoop  48902  lincvalsc0  48912  linc0scn0  48914  lincdifsn  48915  linc1  48916  lspsslco  48928  lincresunit3lem2  48971  lincresunit3  48972