Theorem pweqi 4573

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  rankxplim  9896  pwdju1  10269  fin23lem17  10416  mnfnre  11352  qtopres  24017  hmphdis  24115  ust0  24539  made0  28249  umgrpredgv  29718  lfuhgr  29726  issubgr  29852  uhgrissubgr  29856  cusgredg  30005  cffldtocusgr  30028  konigsbergiedgw  30849  shsspwh  31848  circtopn  34469  r11  35725  r12  35726  rankeq1o  36932  onsucsuccmpi  37231  bj-unirel  37966  elrfi  43704  islmodfg  44070  clsk1indlem4  45043  clsk1indlem1  45044  clsk1independent  45045  omef  47505  caragensplit  47509  caragenelss  47510  carageneld  47511  omeunile  47514  caragensspw  47518  0ome  47538  isomennd  47540  ovn02  47577  isuspgrimlem  48992  grtri  49037  usgrexmpl1lem  49118  usgrexmpl2lem  49123  lcoop  49522  lincvalsc0  49532  linc0scn0  49534  lincdifsn  49535  linc1  49536  lspsslco  49548  lincresunit3lem2  49591  lincresunit3  49592