Theorem pweqi 4576

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  rankxplim  9933  pwdju1  10308  fin23lem17  10455  mnfnre  11391  qtopres  24072  hmphdis  24170  ust0  24594  made0  28306  umgrpredgv  29775  lfuhgr  29783  issubgr  29909  uhgrissubgr  29913  cusgredg  30062  cffldtocusgr  30085  konigsbergiedgw  30906  shsspwh  31905  circtopn  34580  r11  35850  r12  35851  rankeq1o  37147  onsucsuccmpi  37446  bj-unirel  38236  elrfi  43971  islmodfg  44337  clsk1indlem4  45305  clsk1indlem1  45306  clsk1independent  45307  omef  47779  caragensplit  47783  caragenelss  47784  carageneld  47785  omeunile  47788  caragensspw  47792  0ome  47812  isomennd  47814  ovn02  47851  isuspgrimlem  49266  grtri  49311  usgrexmpl1lem  49392  usgrexmpl2lem  49397  lcoop  49854  lincvalsc0  49864  linc0scn0  49866  lincdifsn  49867  linc1  49868  lspsslco  49880  lincresunit3lem2  49923  lincresunit3  49924