Theorem pweqi 4580

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

This proof depends on syntax axioms:   = wceq 1570  𝒫 cpw 4564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-pw 4566

This theorem is used by:  rankxplim  9858  pwdju1  10190  fin23lem17  10337  mnfnre  11269  qtopres  23908  hmphdis  24006  ust0  24430  made0  28109  umgrpredgv  29547  lfuhgr  29555  issubgr  29681  uhgrissubgr  29685  cusgredg  29834  cffldtocusgr  29857  konigsbergiedgw  30672  shsspwh  31671  circtopn  34293  r11  35547  r12  35548  rankeq1o  36702  onsucsuccmpi  37013  bj-unirel  37746  elrfi  43485  islmodfg  43856  clsk1indlem4  44830  clsk1indlem1  44831  clsk1independent  44832  omef  47270  caragensplit  47274  caragenelss  47275  carageneld  47276  omeunile  47279  caragensspw  47283  0ome  47303  isomennd  47305  ovn02  47342  isuspgrimlem  48720  grtri  48765  usgrexmpl1lem  48846  usgrexmpl2lem  48851  lcoop  49250  lincvalsc0  49260  linc0scn0  49262  lincdifsn  49263  linc1  49264  lspsslco  49276  lincresunit3lem2  49319  lincresunit3  49320