Theorem pweqi 4545

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

Syntax hints:   = wceq 1547  𝒫 cpw 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-pw 4531

This theorem is referenced by:  rankxplim  9794  pwdju1  10104  fin23lem17  10251  mnfnre  11179  qtopres  23681  hmphdis  23779  ust0  24203  made0  27873  umgrpredgv  29227  issubgr  29358  uhgrissubgr  29362  cusgredg  29511  cffldtocusgr  29534  konigsbergiedgw  30336  shsspwh  31335  circtopn  34021  r11  35275  r12  35276  lfuhgr  35346  rankeq1o  36399  onsucsuccmpi  36671  bj-unirel  37404  elrfi  43143  islmodfg  43514  clsk1indlem4  44488  clsk1indlem1  44489  clsk1independent  44490  omef  46939  caragensplit  46943  caragenelss  46944  carageneld  46945  omeunile  46948  caragensspw  46952  0ome  46972  isomennd  46974  ovn02  47011  isuspgrimlem  48386  grtri  48431  usgrexmpl1lem  48512  usgrexmpl2lem  48517  lcoop  48902  lincvalsc0  48912  linc0scn0  48914  lincdifsn  48915  linc1  48916  lspsslco  48928  lincresunit3lem2  48971  lincresunit3  48972