Theorem pweq 4581

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 4003	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4580	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4004	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4580	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3962	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1567  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-pw 4569

This theorem is referenced by:  pweqi  4583  pweqd  4584  axpweq  5322  pwexg  5350  pwssun  5554  knatar  7356  pwdom  9116  canth2g  9118  pwfi  9277  fival  9371  marypha1lem  9392  marypha1  9393  wdompwdom  9539  canthwdom  9540  r1sucg  9740  ranklim  9815  r1pwALT  9817  isacn  10027  dfac12r  10129  dfac12k  10130  pwsdompw  10185  ackbij1lem8  10208  ackbij1lem14  10214  r1om  10225  fictb  10226  isfin1a  10275  isfin2  10277  isfin3  10279  isfin3ds  10312  isf33lem  10349  domtriomlem  10425  ttukeylem1  10492  elgch  10606  wunpw  10691  wunex2  10722  wuncval2  10731  eltskg  10734  eltsk2g  10735  tskpwss  10736  tskpw  10737  inar1  10759  grupw  10779  grothpw  10810  grothpwex  10811  axgroth6  10812  grothomex  10813  grothac  10814  indv  12219  axdc4uz  14019  hashpw  14472  hashbc  14489  ackbijnn  15881  incexclem  15889  rami  17074  ismre  17641  isacs  17706  isacs2  17708  acsfiel  17709  isacs1i  17712  mreacs  17713  isssc  17876  acsficl  18602  efmnd  18928  pmtrfval  19519  selvffval  22237  istopg  23020  istopon  23037  eltg  23082  tgdom  23103  ntrval  23161  nrmsep3  23480  iscmp  23513  cmpcov  23514  cmpsublem  23524  cmpsub  23525  tgcmp  23526  uncmp  23528  hauscmplem  23531  is1stc  23566  2ndc1stc  23576  llyi  23599  nllyi  23600  cldllycmp  23620  isfbas  23954  isfil  23972  filss  23978  fgval  23995  elfg  23996  isufil  24028  alexsublem  24169  alexsubb  24171  alexsubALTlem1  24172  alexsubALTlem2  24173  alexsubALTlem4  24175  alexsubALT  24176  restmetu  24695  bndth  25085  ovolicc2  25649  uhgreq12g  29355  uhgr0vb  29362  isupgr  29374  isumgr  29385  isuspgr  29442  isusgr  29443  isausgr  29454  lfuhgr1v0e  29544  nbuhgr2vtx1edgblem  29641  ex-pw  30720  esplyval  33896  iscref  34178  sigaval  34445  issiga  34446  isrnsiga  34447  issgon  34457  isldsys  34490  issros  34509  measval  34532  isrnmeas  34534  rankpwg  36559  neibastop1  36758  neibastop2lem  36759  neibastop2  36760  neibastop3  36761  neifg  36770  limsucncmpi  36844  bj-snglex  37496  bj-ismoore  37634  pibp19  37947  pibt2  37950  cover2g  38254  isnacs  43326  mrefg2  43329  aomclem8  43679  islssfg2  43689  lnr2i  43734  pwelg  44177  fsovd  44625  fsovcnvlem  44630  dssmapfvd  44634  clsk1independent  44663  ntrneibex  44690  mnuop123d  44863  stoweidlem50  46655  stoweidlem57  46662  issal  46919  omessle  47103  grtri  48593  vsetrec  50365  elpglem3  50375  pgindnf  50378