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

Theorem ssexg 5218
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
ssexg ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)

Proof of Theorem ssexg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sseq2 3990 . . . 4 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
21imbi1d 343 . . 3 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ V) ↔ (𝐴𝐵𝐴 ∈ V)))
3 vex 3495 . . . 4 𝑥 ∈ V
43ssex 5216 . . 3 (𝐴𝑥𝐴 ∈ V)
52, 4vtoclg 3565 . 2 (𝐵𝐶 → (𝐴𝐵𝐴 ∈ V))
65impcom 408 1 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  Vcvv 3492  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-in 3940  df-ss 3949
This theorem is referenced by:  ssexd  5219  prcssprc  5220  difexg  5222  rabexg  5225  elssabg  5230  elpw2g  5238  abssexg  5273  snexALT  5274  sess1  5516  sess2  5517  riinint  5832  resexg  5891  trsuc  6268  ordsssuc2  6272  mptexg  6975  mptexgf  6976  isofr2  7086  ofres  7414  brrpssg  7440  unexb  7460  xpexg  7462  abnexg  7467  difex2  7471  uniexr  7474  dmexg  7602  rnexg  7603  resiexg  7608  imaexg  7609  exse2  7611  cnvexg  7618  coexg  7623  fabexg  7628  f1oabexg  7631  resfunexgALT  7638  cofunexg  7639  fnexALT  7641  f1dmex  7647  oprabexd  7665  mpoexxg  7762  suppfnss  7844  tposexg  7895  tz7.48-3  8069  oaabs  8260  erex  8302  mapex  8401  pmvalg  8406  elpmg  8411  elmapssres  8420  pmss12g  8422  ralxpmap  8448  ixpexg  8474  ssdomg  8543  fiprc  8583  domunsncan  8605  infensuc  8683  pssnn  8724  unbnn  8762  fodomfi  8785  fival  8864  fiss  8876  dffi3  8883  hartogslem2  8995  card2on  9006  wdomima2g  9038  unxpwdom2  9040  unxpwdom  9041  harwdom  9042  oemapvali  9135  ackbij1lem11  9640  cofsmo  9679  ssfin4  9720  fin23lem11  9727  ssfin2  9730  ssfin3ds  9740  isfin1-3  9796  hsmex3  9844  axdc2lem  9858  ac6num  9889  ttukeylem1  9919  dmct  9934  ondomon  9973  fpwwe2lem3  10043  fpwwe2lem12  10051  fpwwe2lem13  10052  canthwe  10061  wuncss  10155  genpv  10409  genpdm  10412  hashss  13758  hashf1lem1  13801  wrdexgOLD  13860  wrdexb  13861  shftfval  14417  o1of2  14957  o1rlimmul  14963  isercolllem2  15010  isstruct2  16481  ressval3d  16549  ressabs  16551  prdsbas  16718  fnmrc  16866  mrcfval  16867  isacs1i  16916  mreacs  16917  isssc  17078  ipolerval  17754  ress0g  17927  symgbas  18436  sylow2a  18673  islbs3  19856  toponsspwpw  21458  basdif0  21489  tgval  21491  eltg  21493  eltg2  21494  tgss  21504  basgen2  21525  2basgen  21526  bastop1  21529  topnex  21532  resttopon  21697  restabs  21701  restcld  21708  restfpw  21715  restcls  21717  restntr  21718  ordtbas2  21727  ordtbas  21728  lmfval  21768  cnrest  21821  cmpcov  21925  cmpsublem  21935  cmpsub  21936  2ndcomap  21994  islocfin  22053  txss12  22141  ptrescn  22175  trfbas2  22379  trfbas  22380  isfildlem  22393  snfbas  22402  trfil1  22422  trfil2  22423  trufil  22446  ssufl  22454  hauspwpwf1  22523  ustval  22738  metrest  23061  cnheibor  23486  metcld2  23837  bcthlem1  23854  mbfimaopn2  24185  0pledm  24201  dvbss  24426  dvreslem  24434  dvres2lem  24435  dvcnp2  24444  dvaddbr  24462  dvmulbr  24463  dvcnvrelem2  24542  elply2  24713  plyf  24715  plyss  24716  elplyr  24718  plyeq0lem  24727  plyeq0  24728  plyaddlem  24732  plymullem  24733  dgrlem  24746  coeidlem  24754  ulmcn  24914  pserulm  24937  rabexgfGS  30189  abrexdomjm  30194  aciunf1  30336  ress1r  30787  pcmplfin  31023  metidval  31029  indval  31171  sigagenss  31307  measval  31356  omsfval  31451  omssubaddlem  31456  omssubadd  31457  carsggect  31475  erdsze2lem1  32347  erdsze2lem2  32348  cvxpconn  32386  elmsta  32692  dfon2lem3  32927  altxpexg  33336  ivthALT  33580  filnetlem3  33625  bj-elpwg  34239  bj-restsnss  34268  bj-restsnss2  34269  bj-restb  34279  bj-restuni2  34283  abrexdom  34886  sdclem2  34898  sdclem1  34899  imaexALTV  35468  brssr  35621  pssexg  38990  elrfirn  39170  pwssplit4  39567  hbtlem1  39601  hbtlem7  39603  inaex  40510  rabexgf  41158  disjinfi  41330  dvnprodlem1  42107  dvnprodlem2  42108  qndenserrnbllem  42456  sge0ss  42571  psmeasurelem  42629  caragensplit  42659  omeunile  42664  caragenuncl  42672  omeunle  42675  omeiunlempt  42679  carageniuncllem2  42681  frnvafv2v  43312  prprval  43553  mpoexxg2  44314  gsumlsscl  44359  lincellss  44409
  Copyright terms: Public domain W3C validator