Theorem pweq 4577

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 4005	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4576	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4006	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4576	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3964	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1540  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565

This theorem is referenced by:  pweqi  4579  pweqd  4580  axpweq  5306  pwexg  5333  pwssun  5530  knatar  7332  pwdom  9093  canth2g  9095  pwfi  9268  fival  9363  marypha1lem  9384  marypha1  9385  wdompwdom  9531  canthwdom  9532  r1sucg  9722  ranklim  9797  r1pwALT  9799  isacn  9997  dfac12r  10100  dfac12k  10101  pwsdompw  10156  ackbij1lem8  10179  ackbij1lem14  10185  r1om  10196  fictb  10197  isfin1a  10245  isfin2  10247  isfin3  10249  isfin3ds  10282  isf33lem  10319  domtriomlem  10395  ttukeylem1  10462  elgch  10575  wunpw  10660  wunex2  10691  wuncval2  10700  eltskg  10703  eltsk2g  10704  tskpwss  10705  tskpw  10706  inar1  10728  grupw  10748  grothpw  10779  grothpwex  10780  axgroth6  10781  grothomex  10782  grothac  10783  axdc4uz  13949  hashpw  14401  hashbc  14418  ackbijnn  15794  incexclem  15802  rami  16986  ismre  17551  isacs  17612  isacs2  17614  acsfiel  17615  isacs1i  17618  mreacs  17619  isssc  17782  acsficl  18506  efmnd  18797  pmtrfval  19380  selvffval  22020  istopg  22782  istopon  22799  eltg  22844  tgdom  22865  ntrval  22923  nrmsep3  23242  iscmp  23275  cmpcov  23276  cmpsublem  23286  cmpsub  23287  tgcmp  23288  uncmp  23290  hauscmplem  23293  is1stc  23328  2ndc1stc  23338  llyi  23361  nllyi  23362  cldllycmp  23382  isfbas  23716  isfil  23734  filss  23740  fgval  23757  elfg  23758  isufil  23790  alexsublem  23931  alexsubb  23933  alexsubALTlem1  23934  alexsubALTlem2  23935  alexsubALTlem4  23937  alexsubALT  23938  restmetu  24458  bndth  24857  ovolicc2  25423  uhgreq12g  28992  uhgr0vb  28999  isupgr  29011  isumgr  29022  isuspgr  29079  isusgr  29080  isausgr  29091  lfuhgr1v0e  29181  nbuhgr2vtx1edgblem  29278  ex-pw  30358  indv  32775  iscref  33834  sigaval  34101  issiga  34102  isrnsiga  34103  issgon  34113  isldsys  34146  issros  34165  measval  34188  isrnmeas  34190  rankpwg  36157  neibastop1  36347  neibastop2lem  36348  neibastop2  36349  neibastop3  36350  neifg  36359  limsucncmpi  36433  bj-snglex  36961  bj-ismoore  37093  pibp19  37402  pibt2  37405  cover2g  37710  isnacs  42692  mrefg2  42695  aomclem8  43050  islssfg2  43060  lnr2i  43105  pwelg  43549  fsovd  43997  fsovcnvlem  44002  dssmapfvd  44006  clsk1independent  44035  ntrneibex  44062  mnuop123d  44251  stoweidlem50  46048  stoweidlem57  46055  issal  46312  omessle  46496  grtri  47939  vsetrec  49692  elpglem3  49702  pgindnf  49705