Theorem pweqi 4112

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

Syntax hints:   = wceq 1475  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  pwfi  8144  rankxplim  8625  pwcda1  8899  fin23lem17  9043  mnfnre  9961  qtopres  21311  hmphdis  21409  ust0  21833  umgrpredgav  25813  shsspwh  27487  circtopn  29232  rankeq1o  31448  onsucsuccmpi  31612  elrfi  36275  islmodfg  36657  clsk1indlem4  37362  clsk1indlem1  37363  clsk1independent  37364  omef  39386  caragensplit  39390  caragenelss  39391  carageneld  39392  omeunile  39395  caragensspw  39399  0ome  39419  isomennd  39421  ovn02  39458  issubgr  40495  uhgrissubgr  40499  cusgredg  40646  konigsbergiedgw  41416  konigsbergiedgwOLD  41417  lcoop  41994  lincvalsc0  42004  linc0scn0  42006  lincdifsn  42007  linc1  42008  lspsslco  42020  lincresunit3lem2  42063  lincresunit3  42064