Theorem pweqi 4548

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

Syntax hints:   = wceq 1539  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  pwfiOLD  9044  rankxplim  9568  pwdju1  9877  fin23lem17  10025  mnfnre  10949  qtopres  22757  hmphdis  22855  ust0  23279  umgrpredgv  27413  issubgr  27541  uhgrissubgr  27545  cusgredg  27694  cffldtocusgr  27717  konigsbergiedgw  28513  shsspwh  29509  circtopn  31689  lfuhgr  32979  made0  33984  rankeq1o  34400  onsucsuccmpi  34559  bj-unirel  35151  elrfi  40432  islmodfg  40810  clsk1indlem4  41543  clsk1indlem1  41544  clsk1independent  41545  omef  43924  caragensplit  43928  caragenelss  43929  carageneld  43930  omeunile  43933  caragensspw  43937  0ome  43957  isomennd  43959  ovn02  43996  lcoop  45640  lincvalsc0  45650  linc0scn0  45652  lincdifsn  45653  linc1  45654  lspsslco  45666  lincresunit3lem2  45709  lincresunit3  45710