Theorem pweq 4559

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 3988	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4558	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3989	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4558	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3947	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1541  𝒫 cpw 4545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-pw 4547

This theorem is referenced by:  pweqi  4561  pweqd  4562  axpweq  5284  pwexg  5311  pwssun  5503  knatar  7286  pwdom  9037  canth2g  9039  pwfi  9198  fival  9291  marypha1lem  9312  marypha1  9313  wdompwdom  9459  canthwdom  9460  r1sucg  9657  ranklim  9732  r1pwALT  9734  isacn  9930  dfac12r  10033  dfac12k  10034  pwsdompw  10089  ackbij1lem8  10112  ackbij1lem14  10118  r1om  10129  fictb  10130  isfin1a  10178  isfin2  10180  isfin3  10182  isfin3ds  10215  isf33lem  10252  domtriomlem  10328  ttukeylem1  10395  elgch  10508  wunpw  10593  wunex2  10624  wuncval2  10633  eltskg  10636  eltsk2g  10637  tskpwss  10638  tskpw  10639  inar1  10661  grupw  10681  grothpw  10712  grothpwex  10713  axgroth6  10714  grothomex  10715  grothac  10716  axdc4uz  13886  hashpw  14338  hashbc  14355  ackbijnn  15730  incexclem  15738  rami  16922  ismre  17487  isacs  17552  isacs2  17554  acsfiel  17555  isacs1i  17558  mreacs  17559  isssc  17722  acsficl  18448  efmnd  18773  pmtrfval  19357  selvffval  22043  istopg  22805  istopon  22822  eltg  22867  tgdom  22888  ntrval  22946  nrmsep3  23265  iscmp  23298  cmpcov  23299  cmpsublem  23309  cmpsub  23310  tgcmp  23311  uncmp  23313  hauscmplem  23316  is1stc  23351  2ndc1stc  23361  llyi  23384  nllyi  23385  cldllycmp  23405  isfbas  23739  isfil  23757  filss  23763  fgval  23780  elfg  23781  isufil  23813  alexsublem  23954  alexsubb  23956  alexsubALTlem1  23957  alexsubALTlem2  23958  alexsubALTlem4  23960  alexsubALT  23961  restmetu  24480  bndth  24879  ovolicc2  25445  uhgreq12g  29038  uhgr0vb  29045  isupgr  29057  isumgr  29068  isuspgr  29125  isusgr  29126  isausgr  29137  lfuhgr1v0e  29227  nbuhgr2vtx1edgblem  29324  ex-pw  30401  indv  32825  esplyval  33577  iscref  33849  sigaval  34116  issiga  34117  isrnsiga  34118  issgon  34128  isldsys  34161  issros  34180  measval  34203  isrnmeas  34205  rankpwg  36203  neibastop1  36393  neibastop2lem  36394  neibastop2  36395  neibastop3  36396  neifg  36405  limsucncmpi  36479  bj-snglex  37007  bj-ismoore  37139  pibp19  37448  pibt2  37451  cover2g  37756  isnacs  42737  mrefg2  42740  aomclem8  43094  islssfg2  43104  lnr2i  43149  pwelg  43593  fsovd  44041  fsovcnvlem  44046  dssmapfvd  44050  clsk1independent  44079  ntrneibex  44106  mnuop123d  44295  stoweidlem50  46088  stoweidlem57  46095  issal  46352  omessle  46536  grtri  47971  vsetrec  49735  elpglem3  49745  pgindnf  49748