Theorem pweq 4550

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 3978	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4549	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 3979	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4549	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3939	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1539  𝒫 cpw 4534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-pw 4536

This theorem is referenced by:  pweqi  4552  pweqd  4553  axpweq  5288  pwexg  5302  pwssun  5486  knatar  7237  pwdom  8925  canth2g  8927  pwfi  8970  pwfiOLD  9123  fival  9180  marypha1lem  9201  marypha1  9202  wdompwdom  9346  canthwdom  9347  r1sucg  9536  ranklim  9611  r1pwALT  9613  isacn  9809  dfac12r  9911  dfac12k  9912  pwsdompw  9969  ackbij1lem8  9992  ackbij1lem14  9998  r1om  10009  fictb  10010  isfin1a  10057  isfin2  10059  isfin3  10061  isfin3ds  10094  isf33lem  10131  domtriomlem  10207  ttukeylem1  10274  elgch  10387  wunpw  10472  wunex2  10503  wuncval2  10512  eltskg  10515  eltsk2g  10516  tskpwss  10517  tskpw  10518  inar1  10540  grupw  10560  grothpw  10591  grothpwex  10592  axgroth6  10593  grothomex  10594  grothac  10595  axdc4uz  13713  hashpw  14160  hashbc  14174  ackbijnn  15549  incexclem  15557  rami  16725  ismre  17308  isacs  17369  isacs2  17371  acsfiel  17372  isacs1i  17375  mreacs  17376  isssc  17541  acsficl  18274  efmnd  18518  pmtrfval  19067  selvffval  21335  istopg  22053  istopon  22070  eltg  22116  tgdom  22137  ntrval  22196  nrmsep3  22515  iscmp  22548  cmpcov  22549  cmpsublem  22559  cmpsub  22560  tgcmp  22561  uncmp  22563  hauscmplem  22566  is1stc  22601  2ndc1stc  22611  llyi  22634  nllyi  22635  cldllycmp  22655  isfbas  22989  isfil  23007  filss  23013  fgval  23030  elfg  23031  isufil  23063  alexsublem  23204  alexsubb  23206  alexsubALTlem1  23207  alexsubALTlem2  23208  alexsubALTlem4  23210  alexsubALT  23211  restmetu  23735  bndth  24130  ovolicc2  24695  uhgreq12g  27444  uhgr0vb  27451  isupgr  27463  isumgr  27474  isuspgr  27531  isusgr  27532  isausgr  27543  lfuhgr1v0e  27630  usgrexmpl  27639  nbuhgr2vtx1edgblem  27727  ex-pw  28802  iscref  31803  indv  31989  sigaval  32088  issiga  32089  isrnsiga  32090  issgon  32100  isldsys  32133  issros  32152  measval  32175  isrnmeas  32177  rankpwg  34480  neibastop1  34557  neibastop2lem  34558  neibastop2  34559  neibastop3  34560  neifg  34569  limsucncmpi  34643  bj-snglex  35172  bj-ismoore  35285  pibp19  35594  pibt2  35597  cover2g  35882  isnacs  40533  mrefg2  40536  aomclem8  40893  islssfg2  40903  lnr2i  40948  pwelg  41174  fsovd  41623  fsovcnvlem  41628  dssmapfvd  41632  clsk1independent  41663  ntrneibex  41690  mnuop123d  41887  stoweidlem50  43598  stoweidlem57  43605  issal  43862  omessle  44043  vsetrec  46419  elpglem3  46429