Theorem pweqi 4583

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

Syntax hints:   = wceq 1567  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-pw 4569

This theorem is referenced by:  rankxplim  9850  pwdju1  10173  fin23lem17  10321  mnfnre  11251  qtopres  23823  hmphdis  23921  ust0  24345  made0  28021  umgrpredgv  29430  issubgr  29561  uhgrissubgr  29565  cusgredg  29714  cffldtocusgr  29737  konigsbergiedgw  30539  shsspwh  31538  circtopn  34171  r11  35429  r12  35430  lfuhgr  35508  rankeq1o  36561  onsucsuccmpi  36842  bj-unirel  37574  elrfi  43316  islmodfg  43687  clsk1indlem4  44661  clsk1indlem1  44662  clsk1independent  44663  omef  47101  caragensplit  47105  caragenelss  47106  carageneld  47107  omeunile  47110  caragensspw  47114  0ome  47134  isomennd  47136  ovn02  47173  isuspgrimlem  48548  grtri  48593  usgrexmpl1lem  48674  usgrexmpl2lem  48679  lcoop  49075  lincvalsc0  49085  linc0scn0  49087  lincdifsn  49088  linc1  49089  lspsslco  49101  lincresunit3lem2  49144  lincresunit3  49145