Theorem pweq 4576

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 3995	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4575	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3996	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4575	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3954	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1570  𝒫 cpw 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-pw 4564

This theorem is referenced by:  pweqi  4578  pweqd  4579  axpweq  5321  pwexg  5349  pwssun  5553  knatar  7355  pwdom  9113  canth2g  9115  pwfi  9274  fival  9368  marypha1lem  9389  marypha1  9390  wdompwdom  9536  canthwdom  9537  r1sucg  9737  ranklim  9812  r1pwALT  9814  isacn  10024  dfac12r  10126  dfac12k  10127  pwsdompw  10182  ackbij1lem8  10205  ackbij1lem14  10211  r1om  10222  fictb  10223  isfin1a  10271  isfin2  10273  isfin3  10275  isfin3ds  10308  isf33lem  10345  domtriomlem  10421  ttukeylem1  10488  elgch  10602  wunpw  10687  wunex2  10718  wuncval2  10727  eltskg  10730  eltsk2g  10731  tskpwss  10732  tskpw  10733  inar1  10755  grupw  10775  grothpw  10806  grothpwex  10807  axgroth6  10808  grothomex  10809  grothac  10810  indv  12215  axdc4uz  14016  hashpw  14469  hashbc  14486  ackbijnn  15878  incexclem  15886  rami  17070  ismre  17637  isacs  17702  isacs2  17704  acsfiel  17705  isacs1i  17708  mreacs  17709  isssc  17872  acsficl  18598  efmnd  18924  pmtrfval  19515  selvffval  22269  istopg  23052  istopon  23069  eltg  23114  tgdom  23135  ntrval  23193  nrmsep3  23512  iscmp  23545  cmpcov  23546  cmpsublem  23556  cmpsub  23557  tgcmp  23558  uncmp  23560  hauscmplem  23563  is1stc  23598  2ndc1stc  23608  llyi  23631  nllyi  23632  cldllycmp  23652  isfbas  23986  isfil  24004  filss  24010  fgval  24027  elfg  24028  isufil  24060  alexsublem  24201  alexsubb  24203  alexsubALTlem1  24204  alexsubALTlem2  24205  alexsubALTlem4  24207  alexsubALT  24208  restmetu  24727  bndth  25117  ovolicc2  25681  uhgreq12g  29415  uhgr0vb  29422  isupgr  29434  isumgr  29445  isuspgr  29502  isusgr  29503  isausgr  29514  lfuhgr1v0e  29604  nbuhgr2vtx1edgblem  29701  ex-pw  30780  esplyval  33952  iscref  34234  sigaval  34501  issiga  34502  isrnsiga  34503  issgon  34513  isldsys  34546  issros  34565  measval  34588  isrnmeas  34590  rankpwg  36661  neibastop1  36870  neibastop2lem  36871  neibastop2  36872  neibastop3  36873  neifg  36882  limsucncmpi  36956  bj-snglex  37609  bj-ismoore  37747  pibp19  38060  pibt2  38063  cover2g  38367  isnacs  43435  mrefg2  43438  aomclem8  43788  islssfg2  43798  lnr2i  43843  pwelg  44286  fsovd  44734  fsovcnvlem  44739  dssmapfvd  44743  clsk1independent  44772  ntrneibex  44799  mnuop123d  44972  stoweidlem50  46764  stoweidlem57  46771  issal  47028  omessle  47212  grtri  48705  vsetrec  50481  elpglem3  50491  pgindnf  50494