Theorem pweqi 4307

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

Syntax hints:   = wceq 1632  𝒫 cpw 4303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-in 3723  df-ss 3730  df-pw 4305

This theorem is referenced by:  pwfi  8429  rankxplim  8918  pwcda1  9229  fin23lem17  9373  mnfnre  10295  qtopres  21724  hmphdis  21822  ust0  22245  umgrpredgv  26256  issubgr  26384  uhgrissubgr  26388  cusgredg  26552  cffldtocusgr  26575  konigsbergiedgw  27422  shsspwh  28434  circtopn  30235  rankeq1o  32606  onsucsuccmpi  32770  elrfi  37778  islmodfg  38160  clsk1indlem4  38863  clsk1indlem1  38864  clsk1independent  38865  omef  41235  caragensplit  41239  caragenelss  41240  carageneld  41241  omeunile  41244  caragensspw  41248  0ome  41268  isomennd  41270  ovn02  41307  lcoop  42729  lincvalsc0  42739  linc0scn0  42741  lincdifsn  42742  linc1  42743  lspsslco  42755  lincresunit3lem2  42798  lincresunit3  42799