MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pweq Structured version   Visualization version   GIF version

Theorem pweq 4531
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
StepHypRef Expression
1 eqimss 4002 . . 3 (𝐴 = 𝐵𝐴𝐵)
21sspwd 4530 . 2 (𝐴 = 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3 eqimss2 4003 . . 3 (𝐴 = 𝐵𝐵𝐴)
43sspwd 4530 . 2 (𝐴 = 𝐵 → 𝒫 𝐵 ⊆ 𝒫 𝐴)
52, 4eqssd 3963 1 (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  𝒫 cpw 4515
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 2792
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 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-v 3475  df-in 3920  df-ss 3930  df-pw 4517
This theorem is referenced by:  pweqi  4533  pweqd  4534  axpweq  5241  pwexg  5255  pwssun  5432  knatar  7087  pwdom  8647  canth2g  8649  pwfi  8797  fival  8854  marypha1lem  8875  marypha1  8876  wdompwdom  9020  canthwdom  9021  r1sucg  9176  ranklim  9251  r1pwALT  9253  isacn  9448  dfac12r  9550  dfac12k  9551  pwsdompw  9604  ackbij1lem8  9627  ackbij1lem14  9633  r1om  9644  fictb  9645  isfin1a  9692  isfin2  9694  isfin3  9696  isfin3ds  9729  isf33lem  9766  domtriomlem  9842  ttukeylem1  9909  elgch  10022  wunpw  10107  wunex2  10138  wuncval2  10147  eltskg  10150  eltsk2g  10151  tskpwss  10152  tskpw  10153  inar1  10175  grupw  10195  grothpw  10226  grothpwex  10227  axgroth6  10228  grothomex  10229  grothac  10230  axdc4uz  13336  hashpw  13782  hashbc  13796  ackbijnn  15163  incexclem  15171  rami  16329  ismre  16840  isacs  16901  isacs2  16903  acsfiel  16904  isacs1i  16907  mreacs  16908  isssc  17069  acsficl  17760  efmnd  18014  pmtrfval  18557  selvffval  20305  istopg  21479  istopon  21496  eltg  21541  tgdom  21562  ntrval  21620  nrmsep3  21939  iscmp  21972  cmpcov  21973  cmpsublem  21983  cmpsub  21984  tgcmp  21985  uncmp  21987  hauscmplem  21990  is1stc  22025  2ndc1stc  22035  llyi  22058  nllyi  22059  cldllycmp  22079  isfbas  22413  isfil  22431  filss  22437  fgval  22454  elfg  22455  isufil  22487  alexsublem  22628  alexsubb  22630  alexsubALTlem1  22631  alexsubALTlem2  22632  alexsubALTlem4  22634  alexsubALT  22635  restmetu  23156  bndth  23542  ovolicc2  24105  uhgreq12g  26837  uhgr0vb  26844  isupgr  26856  isumgr  26867  isuspgr  26924  isusgr  26925  isausgr  26936  lfuhgr1v0e  27023  usgrexmpl  27032  nbuhgr2vtx1edgblem  27120  ex-pw  28193  iscref  31119  indv  31279  sigaval  31378  issiga  31379  isrnsiga  31380  issgon  31390  isldsys  31423  issros  31442  measval  31465  isrnmeas  31467  rankpwg  33638  neibastop1  33715  neibastop2lem  33716  neibastop2  33717  neibastop3  33718  neifg  33727  limsucncmpi  33801  bj-snglex  34302  bj-ismoore  34414  pibp19  34712  pibt2  34715  cover2g  35029  isnacs  39438  mrefg2  39441  aomclem8  39798  islssfg2  39808  lnr2i  39853  pwelg  40054  fsovd  40489  fsovcnvlem  40494  dssmapfvd  40498  clsk1independent  40531  ntrneibex  40558  mnuop123d  40753  stoweidlem50  42483  stoweidlem57  42490  issal  42747  omessle  42928  vsetrec  44992  elpglem3  45002
  Copyright terms: Public domain W3C validator