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  9862  pwdju1  10194  fin23lem17  10341  mnfnre  11277  qtopres  23925  hmphdis  24023  ust0  24447  made0  28129  umgrpredgv  29598  lfuhgr  29606  issubgr  29732  uhgrissubgr  29736  cusgredg  29885  cffldtocusgr  29908  konigsbergiedgw  30729  shsspwh  31728  circtopn  34348  r11  35602  r12  35603  rankeq1o  36752  onsucsuccmpi  37063  bj-unirel  37796  elrfi  43540  islmodfg  43911  clsk1indlem4  44885  clsk1indlem1  44886  clsk1independent  44887  omef  47325  caragensplit  47329  caragenelss  47330  carageneld  47331  omeunile  47334  caragensspw  47338  0ome  47358  isomennd  47360  ovn02  47397  isuspgrimlem  48812  grtri  48857  usgrexmpl1lem  48938  usgrexmpl2lem  48943  lcoop  49342  lincvalsc0  49352  linc0scn0  49354  lincdifsn  49355  linc1  49356  lspsslco  49368  lincresunit3lem2  49411  lincresunit3  49412