Theorem pweqi 4571

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

Syntax hints:   = wceq 1560  𝒫 cpw 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-pw 4557

This theorem is referenced by:  rankxplim  9837  pwdju1  10147  fin23lem17  10295  mnfnre  11225  qtopres  23758  hmphdis  23856  ust0  24280  made0  27956  umgrpredgv  29341  issubgr  29472  uhgrissubgr  29476  cusgredg  29625  cffldtocusgr  29648  konigsbergiedgw  30450  shsspwh  31449  circtopn  34134  r11  35390  r12  35391  lfuhgr  35468  rankeq1o  36521  onsucsuccmpi  36803  bj-unirel  37536  elrfi  43275  islmodfg  43646  clsk1indlem4  44620  clsk1indlem1  44621  clsk1independent  44622  omef  47070  caragensplit  47074  caragenelss  47075  carageneld  47076  omeunile  47079  caragensspw  47083  0ome  47103  isomennd  47105  ovn02  47142  isuspgrimlem  48517  grtri  48562  usgrexmpl1lem  48643  usgrexmpl2lem  48648  lcoop  49033  lincvalsc0  49043  linc0scn0  49045  lincdifsn  49046  linc1  49047  lspsslco  49059  lincresunit3lem2  49102  lincresunit3  49103