Theorem pweqi 4619

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

Syntax hints:   = wceq 1542  𝒫 cpw 4603

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  pwfiOLD  9347  rankxplim  9874  pwdju1  10185  fin23lem17  10333  mnfnre  11257  qtopres  23202  hmphdis  23300  ust0  23724  made0  27368  umgrpredgv  28400  issubgr  28528  uhgrissubgr  28532  cusgredg  28681  cffldtocusgr  28704  konigsbergiedgw  29501  shsspwh  30499  circtopn  32817  lfuhgr  34108  rankeq1o  35143  onsucsuccmpi  35328  bj-unirel  35932  elrfi  41432  islmodfg  41811  clsk1indlem4  42795  clsk1indlem1  42796  clsk1independent  42797  omef  45212  caragensplit  45216  caragenelss  45217  carageneld  45218  omeunile  45221  caragensspw  45225  0ome  45245  isomennd  45247  ovn02  45284  lcoop  47092  lincvalsc0  47102  linc0scn0  47104  lincdifsn  47105  linc1  47106  lspsslco  47118  lincresunit3lem2  47161  lincresunit3  47162