Theorem pweq 4616

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 4040	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4615	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4041	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4615	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3999	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  pweqi  4618  pweqd  4619  axpweq  5348  pwexg  5376  pwssun  5571  knatar  7353  pwdom  9128  canth2g  9130  pwfi  9177  pwfiOLD  9346  fival  9406  marypha1lem  9427  marypha1  9428  wdompwdom  9572  canthwdom  9573  r1sucg  9763  ranklim  9838  r1pwALT  9840  isacn  10038  dfac12r  10140  dfac12k  10141  pwsdompw  10198  ackbij1lem8  10221  ackbij1lem14  10227  r1om  10238  fictb  10239  isfin1a  10286  isfin2  10288  isfin3  10290  isfin3ds  10323  isf33lem  10360  domtriomlem  10436  ttukeylem1  10503  elgch  10616  wunpw  10701  wunex2  10732  wuncval2  10741  eltskg  10744  eltsk2g  10745  tskpwss  10746  tskpw  10747  inar1  10769  grupw  10789  grothpw  10820  grothpwex  10821  axgroth6  10822  grothomex  10823  grothac  10824  axdc4uz  13948  hashpw  14395  hashbc  14411  ackbijnn  15773  incexclem  15781  rami  16947  ismre  17533  isacs  17594  isacs2  17596  acsfiel  17597  isacs1i  17600  mreacs  17601  isssc  17766  acsficl  18499  efmnd  18750  pmtrfval  19317  selvffval  21678  istopg  22396  istopon  22413  eltg  22459  tgdom  22480  ntrval  22539  nrmsep3  22858  iscmp  22891  cmpcov  22892  cmpsublem  22902  cmpsub  22903  tgcmp  22904  uncmp  22906  hauscmplem  22909  is1stc  22944  2ndc1stc  22954  llyi  22977  nllyi  22978  cldllycmp  22998  isfbas  23332  isfil  23350  filss  23356  fgval  23373  elfg  23374  isufil  23406  alexsublem  23547  alexsubb  23549  alexsubALTlem1  23550  alexsubALTlem2  23551  alexsubALTlem4  23553  alexsubALT  23554  restmetu  24078  bndth  24473  ovolicc2  25038  uhgreq12g  28322  uhgr0vb  28329  isupgr  28341  isumgr  28352  isuspgr  28409  isusgr  28410  isausgr  28421  lfuhgr1v0e  28508  usgrexmpl  28517  nbuhgr2vtx1edgblem  28605  ex-pw  29679  iscref  32819  indv  33005  sigaval  33104  issiga  33105  isrnsiga  33106  issgon  33116  isldsys  33149  issros  33168  measval  33191  isrnmeas  33193  rankpwg  35136  neibastop1  35239  neibastop2lem  35240  neibastop2  35241  neibastop3  35242  neifg  35251  limsucncmpi  35325  bj-snglex  35849  bj-ismoore  35981  pibp19  36290  pibt2  36293  cover2g  36579  isnacs  41432  mrefg2  41435  aomclem8  41793  islssfg2  41803  lnr2i  41848  pwelg  42301  fsovd  42749  fsovcnvlem  42754  dssmapfvd  42758  clsk1independent  42787  ntrneibex  42814  mnuop123d  43011  stoweidlem50  44756  stoweidlem57  44763  issal  45020  omessle  45204  vsetrec  47738  elpglem3  47748  pgindnf  47751