Theorem pweq 4589

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 4017	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4588	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4018	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4588	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3976	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-pw 4577

This theorem is referenced by:  pweqi  4591  pweqd  4592  axpweq  5321  pwexg  5348  pwssun  5545  knatar  7350  pwdom  9143  canth2g  9145  pwfi  9329  fival  9424  marypha1lem  9445  marypha1  9446  wdompwdom  9592  canthwdom  9593  r1sucg  9783  ranklim  9858  r1pwALT  9860  isacn  10058  dfac12r  10161  dfac12k  10162  pwsdompw  10217  ackbij1lem8  10240  ackbij1lem14  10246  r1om  10257  fictb  10258  isfin1a  10306  isfin2  10308  isfin3  10310  isfin3ds  10343  isf33lem  10380  domtriomlem  10456  ttukeylem1  10523  elgch  10636  wunpw  10721  wunex2  10752  wuncval2  10761  eltskg  10764  eltsk2g  10765  tskpwss  10766  tskpw  10767  inar1  10789  grupw  10809  grothpw  10840  grothpwex  10841  axgroth6  10842  grothomex  10843  grothac  10844  axdc4uz  14002  hashpw  14454  hashbc  14471  ackbijnn  15844  incexclem  15852  rami  17035  ismre  17602  isacs  17663  isacs2  17665  acsfiel  17666  isacs1i  17669  mreacs  17670  isssc  17833  acsficl  18557  efmnd  18848  pmtrfval  19431  selvffval  22071  istopg  22833  istopon  22850  eltg  22895  tgdom  22916  ntrval  22974  nrmsep3  23293  iscmp  23326  cmpcov  23327  cmpsublem  23337  cmpsub  23338  tgcmp  23339  uncmp  23341  hauscmplem  23344  is1stc  23379  2ndc1stc  23389  llyi  23412  nllyi  23413  cldllycmp  23433  isfbas  23767  isfil  23785  filss  23791  fgval  23808  elfg  23809  isufil  23841  alexsublem  23982  alexsubb  23984  alexsubALTlem1  23985  alexsubALTlem2  23986  alexsubALTlem4  23988  alexsubALT  23989  restmetu  24509  bndth  24908  ovolicc2  25475  uhgreq12g  29044  uhgr0vb  29051  isupgr  29063  isumgr  29074  isuspgr  29131  isusgr  29132  isausgr  29143  lfuhgr1v0e  29233  nbuhgr2vtx1edgblem  29330  ex-pw  30410  indv  32829  iscref  33875  sigaval  34142  issiga  34143  isrnsiga  34144  issgon  34154  isldsys  34187  issros  34206  measval  34229  isrnmeas  34231  rankpwg  36187  neibastop1  36377  neibastop2lem  36378  neibastop2  36379  neibastop3  36380  neifg  36389  limsucncmpi  36463  bj-snglex  36991  bj-ismoore  37123  pibp19  37432  pibt2  37435  cover2g  37740  isnacs  42727  mrefg2  42730  aomclem8  43085  islssfg2  43095  lnr2i  43140  pwelg  43584  fsovd  44032  fsovcnvlem  44037  dssmapfvd  44041  clsk1independent  44070  ntrneibex  44097  mnuop123d  44286  stoweidlem50  46079  stoweidlem57  46086  issal  46343  omessle  46527  grtri  47952  vsetrec  49567  elpglem3  49577  pgindnf  49580