Theorem pweq 4573

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 4002	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4572	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4003	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4572	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3961	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

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

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 3446  df-ss 3928  df-pw 4561

This theorem is referenced by:  pweqi  4575  pweqd  4576  axpweq  5301  pwexg  5328  pwssun  5523  knatar  7314  pwdom  9070  canth2g  9072  pwfi  9244  fival  9339  marypha1lem  9360  marypha1  9361  wdompwdom  9507  canthwdom  9508  r1sucg  9698  ranklim  9773  r1pwALT  9775  isacn  9973  dfac12r  10076  dfac12k  10077  pwsdompw  10132  ackbij1lem8  10155  ackbij1lem14  10161  r1om  10172  fictb  10173  isfin1a  10221  isfin2  10223  isfin3  10225  isfin3ds  10258  isf33lem  10295  domtriomlem  10371  ttukeylem1  10438  elgch  10551  wunpw  10636  wunex2  10667  wuncval2  10676  eltskg  10679  eltsk2g  10680  tskpwss  10681  tskpw  10682  inar1  10704  grupw  10724  grothpw  10755  grothpwex  10756  axgroth6  10757  grothomex  10758  grothac  10759  axdc4uz  13925  hashpw  14377  hashbc  14394  ackbijnn  15770  incexclem  15778  rami  16962  ismre  17527  isacs  17588  isacs2  17590  acsfiel  17591  isacs1i  17594  mreacs  17595  isssc  17758  acsficl  18482  efmnd  18773  pmtrfval  19356  selvffval  21996  istopg  22758  istopon  22775  eltg  22820  tgdom  22841  ntrval  22899  nrmsep3  23218  iscmp  23251  cmpcov  23252  cmpsublem  23262  cmpsub  23263  tgcmp  23264  uncmp  23266  hauscmplem  23269  is1stc  23304  2ndc1stc  23314  llyi  23337  nllyi  23338  cldllycmp  23358  isfbas  23692  isfil  23710  filss  23716  fgval  23733  elfg  23734  isufil  23766  alexsublem  23907  alexsubb  23909  alexsubALTlem1  23910  alexsubALTlem2  23911  alexsubALTlem4  23913  alexsubALT  23914  restmetu  24434  bndth  24833  ovolicc2  25399  uhgreq12g  28968  uhgr0vb  28975  isupgr  28987  isumgr  28998  isuspgr  29055  isusgr  29056  isausgr  29067  lfuhgr1v0e  29157  nbuhgr2vtx1edgblem  29254  ex-pw  30331  indv  32748  iscref  33807  sigaval  34074  issiga  34075  isrnsiga  34076  issgon  34086  isldsys  34119  issros  34138  measval  34161  isrnmeas  34163  rankpwg  36130  neibastop1  36320  neibastop2lem  36321  neibastop2  36322  neibastop3  36323  neifg  36332  limsucncmpi  36406  bj-snglex  36934  bj-ismoore  37066  pibp19  37375  pibt2  37378  cover2g  37683  isnacs  42665  mrefg2  42668  aomclem8  43023  islssfg2  43033  lnr2i  43078  pwelg  43522  fsovd  43970  fsovcnvlem  43975  dssmapfvd  43979  clsk1independent  44008  ntrneibex  44035  mnuop123d  44224  stoweidlem50  46021  stoweidlem57  46028  issal  46285  omessle  46469  grtri  47912  vsetrec  49665  elpglem3  49675  pgindnf  49678