Theorem pweq 4543

Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.)

Assertion

Ref	Expression
pweq	⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Proof of Theorem pweq

Step	Hyp	Ref	Expression
1		eqimss 3973	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4542	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3974	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4542	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3932	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = 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:  pweqi  4545  pweqd  4546  axpweq  5279  pwexg  5307  pwssun  5510  knatar  7301  pwdom  9057  canth2g  9059  pwfi  9219  fival  9315  marypha1lem  9336  marypha1  9337  wdompwdom  9483  canthwdom  9484  r1sucg  9684  ranklim  9759  r1pwALT  9761  isacn  9957  dfac12r  10060  dfac12k  10061  pwsdompw  10116  ackbij1lem8  10139  ackbij1lem14  10145  r1om  10156  fictb  10157  isfin1a  10205  isfin2  10207  isfin3  10209  isfin3ds  10242  isf33lem  10279  domtriomlem  10355  ttukeylem1  10422  elgch  10536  wunpw  10621  wunex2  10652  wuncval2  10661  eltskg  10664  eltsk2g  10665  tskpwss  10666  tskpw  10667  inar1  10689  grupw  10709  grothpw  10740  grothpwex  10741  axgroth6  10742  grothomex  10743  grothac  10744  indv  12152  axdc4uz  13937  hashpw  14389  hashbc  14406  ackbijnn  15784  incexclem  15792  rami  16977  ismre  17543  isacs  17608  isacs2  17610  acsfiel  17611  isacs1i  17614  mreacs  17615  isssc  17778  acsficl  18504  efmnd  18829  pmtrfval  19416  selvffval  22094  istopg  22878  istopon  22895  eltg  22940  tgdom  22961  ntrval  23019  nrmsep3  23338  iscmp  23371  cmpcov  23372  cmpsublem  23382  cmpsub  23383  tgcmp  23384  uncmp  23386  hauscmplem  23389  is1stc  23424  2ndc1stc  23434  llyi  23457  nllyi  23458  cldllycmp  23478  isfbas  23812  isfil  23830  filss  23836  fgval  23853  elfg  23854  isufil  23886  alexsublem  24027  alexsubb  24029  alexsubALTlem1  24030  alexsubALTlem2  24031  alexsubALTlem4  24033  alexsubALT  24034  restmetu  24553  bndth  24943  ovolicc2  25507  uhgreq12g  29152  uhgr0vb  29159  isupgr  29171  isumgr  29182  isuspgr  29239  isusgr  29240  isausgr  29251  lfuhgr1v0e  29341  nbuhgr2vtx1edgblem  29438  ex-pw  30517  esplyval  33746  iscref  34028  sigaval  34295  issiga  34296  isrnsiga  34297  issgon  34307  isldsys  34340  issros  34359  measval  34382  isrnmeas  34384  rankpwg  36397  neibastop1  36587  neibastop2lem  36588  neibastop2  36589  neibastop3  36590  neifg  36599  limsucncmpi  36673  bj-snglex  37326  bj-ismoore  37463  pibp19  37776  pibt2  37779  cover2g  38083  isnacs  43153  mrefg2  43156  aomclem8  43506  islssfg2  43516  lnr2i  43561  pwelg  44004  fsovd  44452  fsovcnvlem  44457  dssmapfvd  44461  clsk1independent  44490  ntrneibex  44517  mnuop123d  44706  stoweidlem50  46493  stoweidlem57  46500  issal  46757  omessle  46941  grtri  48431  vsetrec  50193  elpglem3  50203  pgindnf  50206