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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-pw 4559

This theorem is used by:  rankxplim  9861  pwdju1  10193  fin23lem17  10340  mnfnre  11276  qtopres  23924  hmphdis  24022  ust0  24446  made0  28128  umgrpredgv  29597  lfuhgr  29605  issubgr  29731  uhgrissubgr  29735  cusgredg  29884  cffldtocusgr  29907  konigsbergiedgw  30728  shsspwh  31727  circtopn  34347  r11  35601  r12  35602  rankeq1o  36751  onsucsuccmpi  37062  bj-unirel  37795  elrfi  43539  islmodfg  43910  clsk1indlem4  44884  clsk1indlem1  44885  clsk1independent  44886  omef  47324  caragensplit  47328  caragenelss  47329  carageneld  47330  omeunile  47333  caragensspw  47337  0ome  47357  isomennd  47359  ovn02  47396  isuspgrimlem  48811  grtri  48856  usgrexmpl1lem  48937  usgrexmpl2lem  48942  lcoop  49341  lincvalsc0  49351  linc0scn0  49353  lincdifsn  49354  linc1  49355  lspsslco  49367  lincresunit3lem2  49410  lincresunit3  49411