Theorem pweq 4574

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 3971	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4573	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3972	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4573	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3930	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  pweqi  4576  pweqd  4577  axpweq  5319  pwexg  5347  pwssun  5550  knatar  7398  pwdom  9186  canth2g  9188  pwfi  9348  fival  9441  marypha1lem  9462  marypha1  9463  wdompwdom  9609  canthwdom  9610  r1sucg  9813  rankpwg  9894  ranklim  9895  r1pwALT  9897  isacn  10162  dfac12r  10264  dfac12k  10265  pwsdompw  10320  ackbij1lem8  10343  ackbij1lem14  10349  hfom  10360  fictb  10361  isfin1a  10409  isfin2  10411  isfin3  10413  isfin3ds  10446  isf33lem  10483  domtriomlem  10559  ttukeylem1  10626  elgch  10746  wunpw  10831  wunex2  10862  wuncval2  10871  eltskg  10874  eltsk2g  10875  tskpwss  10876  tskpw  10877  inar1  10899  grupw  10919  grothpw  10950  grothpwex  10951  axgroth6  10952  grothomex  10953  grothac  10954  indv  12362  axdc4uz  14167  hashpw  14622  hashbc  14639  ackbijnn  16041  incexclem  16049  rami  17237  ismre  17810  isacs  17875  isacs2  17877  acsfiel  17878  isacs1i  17881  mreacs  17882  isssc  18045  acsficl  18771  efmnd  19116  pmtrfval  19715  selvffval  22482  istopg  23268  istopon  23285  eltg  23330  tgdom  23351  ntrval  23409  nrmsep3  23728  iscmp  23761  cmpcov  23762  cmpsublem  23772  cmpsub  23773  tgcmp  23774  uncmp  23776  hauscmplem  23779  is1stc  23814  2ndc1stc  23824  llyi  23848  nllyi  23849  cldllycmp  23869  isfbas  24203  isfil  24221  filss  24227  fgval  24244  elfg  24245  isufil  24277  alexsublem  24418  alexsubb  24420  alexsubALTlem1  24421  alexsubALTlem2  24422  alexsubALTlem4  24424  alexsubALT  24425  restmetu  24944  bndth  25334  ovolicc2  25898  uhgreq12g  29700  uhgr0vb  29707  isupgr  29719  isumgr  29730  isuspgr  29790  isusgr  29791  isausgr  29802  lfuhgr1v0e  29892  nbuhgr2vtx1edgblem  29989  ex-pw  31087  esplyval  34305  iscref  34587  sigaval  34854  issiga  34855  isrnsiga  34856  issgon  34866  isldsys  34900  issros  34919  measval  34942  isrnmeas  34944  neibastop1  37362  neibastop2lem  37363  neibastop2  37364  neibastop3  37365  neifg  37374  limsucncmpi  37448  bj-snglex  38101  bj-ismoore  38296  pibp19  38605  pibt2  38608  cover2g  38918  isnacs  43981  mrefg2  43984  aomclem8  44329  islssfg2  44339  lnr2i  44383  pwelg  44822  fsovd  45269  fsovcnvlem  45274  dssmapfvd  45278  clsk1independent  45307  ntrneibex  45334  mnuop123d  45507  ackbij3  46289  stoweidlem50  47333  stoweidlem57  47340  issal  47597  omessle  47781  grtri  49311  vsetrec  51202  elpglem3  51212  pgindnf  51215