Theorem pweq 4555

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 4023	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	sspwd 4554	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3		eqimss2 4024	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
4	3	sspwd 4554	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
5	2, 4	eqssd 3984	1 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1537  𝒫 cpw 4539

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  pweqi  4557  pweqd  4558  axpweq  5265  pwexg  5279  pwssun  5456  knatar  7110  pwdom  8669  canth2g  8671  pwfi  8819  fival  8876  marypha1lem  8897  marypha1  8898  wdompwdom  9042  canthwdom  9043  r1sucg  9198  ranklim  9273  r1pwALT  9275  isacn  9470  dfac12r  9572  dfac12k  9573  pwsdompw  9626  ackbij1lem8  9649  ackbij1lem14  9655  r1om  9666  fictb  9667  isfin1a  9714  isfin2  9716  isfin3  9718  isfin3ds  9751  isf33lem  9788  domtriomlem  9864  ttukeylem1  9931  elgch  10044  wunpw  10129  wunex2  10160  wuncval2  10169  eltskg  10172  eltsk2g  10173  tskpwss  10174  tskpw  10175  inar1  10197  grupw  10217  grothpw  10248  grothpwex  10249  axgroth6  10250  grothomex  10251  grothac  10252  axdc4uz  13353  hashpw  13798  hashbc  13812  ackbijnn  15183  incexclem  15191  rami  16351  ismre  16861  isacs  16922  isacs2  16924  acsfiel  16925  isacs1i  16928  mreacs  16929  isssc  17090  acsficl  17781  efmnd  18035  pmtrfval  18578  selvffval  20329  istopg  21503  istopon  21520  eltg  21565  tgdom  21586  ntrval  21644  nrmsep3  21963  iscmp  21996  cmpcov  21997  cmpsublem  22007  cmpsub  22008  tgcmp  22009  uncmp  22011  hauscmplem  22014  is1stc  22049  2ndc1stc  22059  llyi  22082  nllyi  22083  cldllycmp  22103  isfbas  22437  isfil  22455  filss  22461  fgval  22478  elfg  22479  isufil  22511  alexsublem  22652  alexsubb  22654  alexsubALTlem1  22655  alexsubALTlem2  22656  alexsubALTlem4  22658  alexsubALT  22659  restmetu  23180  bndth  23562  ovolicc2  24123  uhgreq12g  26850  uhgr0vb  26857  isupgr  26869  isumgr  26880  isuspgr  26937  isusgr  26938  isausgr  26949  lfuhgr1v0e  27036  usgrexmpl  27045  nbuhgr2vtx1edgblem  27133  ex-pw  28208  iscref  31108  indv  31271  sigaval  31370  issiga  31371  isrnsiga  31372  issgon  31382  isldsys  31415  issros  31434  measval  31457  isrnmeas  31459  rankpwg  33630  neibastop1  33707  neibastop2lem  33708  neibastop2  33709  neibastop3  33710  neifg  33719  limsucncmpi  33793  bj-snglex  34288  bj-ismoore  34400  pibp19  34698  pibt2  34701  cover2g  35005  isnacs  39321  mrefg2  39324  aomclem8  39681  islssfg2  39691  lnr2i  39736  pwelg  39939  fsovd  40374  fsovcnvlem  40379  dssmapfvd  40383  clsk1independent  40416  ntrneibex  40443  mnuop123d  40618  stoweidlem50  42355  stoweidlem57  42362  issal  42619  omessle  42800  vsetrec  44825  elpglem3  44835