Theorem pweqi 4551

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

Syntax hints:   = wceq 1539  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  pwfiOLD  9114  rankxplim  9637  pwdju1  9946  fin23lem17  10094  mnfnre  11018  qtopres  22849  hmphdis  22947  ust0  23371  umgrpredgv  27510  issubgr  27638  uhgrissubgr  27642  cusgredg  27791  cffldtocusgr  27814  konigsbergiedgw  28612  shsspwh  29608  circtopn  31787  lfuhgr  33079  made0  34057  rankeq1o  34473  onsucsuccmpi  34632  bj-unirel  35224  elrfi  40516  islmodfg  40894  clsk1indlem4  41654  clsk1indlem1  41655  clsk1independent  41656  omef  44034  caragensplit  44038  caragenelss  44039  carageneld  44040  omeunile  44043  caragensspw  44047  0ome  44067  isomennd  44069  ovn02  44106  lcoop  45752  lincvalsc0  45762  linc0scn0  45764  lincdifsn  45765  linc1  45766  lspsslco  45778  lincresunit3lem2  45821  lincresunit3  45822