Theorem pweq 4570

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 3967	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4569	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3968	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4569	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3926	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-pw 4558

This theorem is used by:  pweqi  4572  pweqd  4573  axpweq  5312  pwexg  5340  pwssun  5543  knatar  7371  pwdom  9156  canth2g  9158  pwfi  9318  fival  9411  marypha1lem  9432  marypha1  9433  wdompwdom  9579  canthwdom  9580  r1sucg  9783  rankpwg  9864  ranklim  9865  r1pwALT  9867  isacn  10130  dfac12r  10232  dfac12k  10233  pwsdompw  10288  ackbij1lem8  10311  ackbij1lem14  10317  hfom  10328  fictb  10329  isfin1a  10377  isfin2  10379  isfin3  10381  isfin3ds  10414  isf33lem  10451  domtriomlem  10527  ttukeylem1  10594  elgch  10714  wunpw  10799  wunex2  10830  wuncval2  10839  eltskg  10842  eltsk2g  10843  tskpwss  10844  tskpw  10845  inar1  10867  grupw  10887  grothpw  10918  grothpwex  10919  axgroth6  10920  grothomex  10921  grothac  10922  indv  12329  axdc4uz  14134  hashpw  14588  hashbc  14605  ackbijnn  16006  incexclem  16014  rami  17202  ismre  17769  isacs  17834  isacs2  17836  acsfiel  17837  isacs1i  17840  mreacs  17841  isssc  18004  acsficl  18730  efmnd  19075  pmtrfval  19673  selvffval  22436  istopg  23222  istopon  23239  eltg  23284  tgdom  23305  ntrval  23363  nrmsep3  23682  iscmp  23715  cmpcov  23716  cmpsublem  23726  cmpsub  23727  tgcmp  23728  uncmp  23730  hauscmplem  23733  is1stc  23768  2ndc1stc  23778  llyi  23802  nllyi  23803  cldllycmp  23823  isfbas  24157  isfil  24175  filss  24181  fgval  24198  elfg  24199  isufil  24231  alexsublem  24372  alexsubb  24374  alexsubALTlem1  24375  alexsubALTlem2  24376  alexsubALTlem4  24378  alexsubALT  24379  restmetu  24898  bndth  25288  ovolicc2  25852  uhgreq12g  29652  uhgr0vb  29659  isupgr  29671  isumgr  29682  isuspgr  29742  isusgr  29743  isausgr  29754  lfuhgr1v0e  29844  nbuhgr2vtx1edgblem  29941  ex-pw  31039  esplyval  34244  iscref  34526  sigaval  34793  issiga  34794  isrnsiga  34795  issgon  34805  isldsys  34839  issros  34858  measval  34881  isrnmeas  34883  neibastop1  37271  neibastop2lem  37272  neibastop2  37273  neibastop3  37274  neifg  37283  limsucncmpi  37357  bj-snglex  38010  bj-ismoore  38162  pibp19  38474  pibt2  38477  cover2g  38787  isnacs  43852  mrefg2  43855  aomclem8  44200  islssfg2  44210  lnr2i  44255  pwelg  44698  fsovd  45145  fsovcnvlem  45150  dssmapfvd  45154  clsk1independent  45183  ntrneibex  45210  mnuop123d  45383  stoweidlem50  47196  stoweidlem57  47203  issal  47460  omessle  47644  grtri  49174  vsetrec  51007  elpglem3  51017  pgindnf  51020