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

Theorem ssexg 5079
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 3876 . . . 4 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
21imbi1d 334 . . 3 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ V) ↔ (𝐴𝐵𝐴 ∈ V)))
3 vex 3411 . . . 4 𝑥 ∈ V
43ssex 5077 . . 3 (𝐴𝑥𝐴 ∈ V)
52, 4vtoclg 3479 . 2 (𝐵𝐶 → (𝐴𝐵𝐴 ∈ V))
65impcom 399 1 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1508  wcel 2051  Vcvv 3408  wss 3822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743  ax-sep 5056
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-v 3410  df-in 3829  df-ss 3836
This theorem is referenced by:  ssexd  5080  prcssprc  5081  difexg  5083  rabexg  5086  elssabg  5091  elpw2g  5099  abssexg  5131  snexALT  5132  sess1  5371  sess2  5372  riinint  5678  resexg  5740  trsuc  6110  ordsssuc2  6114  mptexg  6808  mptexgf  6809  isofr2  6918  ofres  7241  brrpssg  7267  unexb  7286  xpexg  7288  abnexg  7293  difex2  7297  uniexr  7300  dmexg  7426  rnexg  7427  resiexg  7432  imaexg  7433  exse2  7435  cnvexg  7442  coexg  7447  fabexg  7452  f1oabexg  7455  resfunexgALT  7459  cofunexg  7460  fnexALT  7462  f1dmex  7468  oprabexd  7486  mpoexxg  7579  suppfnss  7656  tposexg  7707  tz7.48-3  7881  oaabs  8069  erex  8111  mapex  8210  pmvalg  8215  elpmg  8220  elmapssres  8229  pmss12g  8231  ralxpmap  8256  ixpexg  8281  ssdomg  8350  fiprc  8390  domunsncan  8411  infensuc  8489  pssnn  8529  unbnn  8567  fodomfi  8590  fival  8669  fiss  8681  dffi3  8688  hartogslem2  8800  card2on  8811  wdomima2g  8843  unxpwdom2  8845  unxpwdom  8846  harwdom  8847  oemapvali  8939  ackbij1lem11  9448  cofsmo  9487  ssfin4  9528  fin23lem11  9535  ssfin2  9538  ssfin3ds  9548  isfin1-3  9604  hsmex3  9652  axdc2lem  9666  ac6num  9697  ttukeylem1  9727  dmct  9742  ondomon  9781  fpwwe2lem3  9851  fpwwe2lem12  9859  fpwwe2lem13  9860  canthwe  9869  wuncss  9963  genpv  10217  genpdm  10220  hashss  13581  hashf1lem1  13624  wrdexgOLD  13681  wrdexb  13682  shftfval  14288  o1of2  14828  o1rlimmul  14834  isercolllem2  14881  isstruct2  16347  ressval3d  16415  ressabs  16417  prdsbas  16584  fnmrc  16748  mrcfval  16749  isacs1i  16798  mreacs  16799  isssc  16960  ipolerval  17636  ress0g  17799  symgbas  18281  sylow2a  18517  islbs3  19661  toponsspwpw  21249  basdif0  21280  tgval  21282  eltg  21284  eltg2  21285  tgss  21295  basgen2  21316  2basgen  21317  bastop1  21320  topnex  21323  resttopon  21488  restabs  21492  restcld  21499  restfpw  21506  restcls  21508  restntr  21509  ordtbas2  21518  ordtbas  21519  lmfval  21559  cnrest  21612  cmpcov  21716  cmpsublem  21726  cmpsub  21727  2ndcomap  21785  islocfin  21844  txss12  21932  ptrescn  21966  trfbas2  22170  trfbas  22171  isfildlem  22184  snfbas  22193  trfil1  22213  trfil2  22214  trufil  22237  ssufl  22245  hauspwpwf1  22314  ustval  22529  metrest  22852  cnheibor  23277  metcld2  23628  bcthlem1  23645  mbfimaopn2  23976  0pledm  23992  dvbss  24217  dvreslem  24225  dvres2lem  24226  dvcnp2  24235  dvaddbr  24253  dvmulbr  24254  dvcnvrelem2  24333  elply2  24504  plyf  24506  plyss  24507  elplyr  24509  plyeq0lem  24518  plyeq0  24519  plyaddlem  24523  plymullem  24524  dgrlem  24537  coeidlem  24545  ulmcn  24705  pserulm  24728  rabexgfGS  30056  abrexdomjm  30061  aciunf1  30187  ress1r  30571  pcmplfin  30800  metidval  30806  indval  30948  sigagenss  31085  measval  31134  omsfval  31229  omssubaddlem  31234  omssubadd  31235  carsggect  31253  erdsze2lem1  32072  erdsze2lem2  32073  cvxpconn  32111  elmsta  32352  dfon2lem3  32587  altxpexg  32997  ivthALT  33241  filnetlem3  33286  bj-restsnss  33921  bj-restsnss2  33922  bj-restb  33932  bj-restuni2  33936  abrexdom  34484  sdclem2  34496  sdclem1  34497  imaexALTV  35069  brssr  35223  pssexg  38595  elrfirn  38725  pwssplit4  39123  hbtlem1  39157  hbtlem7  39159  inaex  40046  rabexgf  40738  disjinfi  40913  dvnprodlem1  41695  dvnprodlem2  41696  qndenserrnbllem  42044  sge0ss  42159  psmeasurelem  42217  caragensplit  42247  omeunile  42252  caragenuncl  42260  omeunle  42263  omeiunlempt  42267  carageniuncllem2  42269  frnvafv2v  42875  prprval  43078  mpoexxg2  43784  gsumlsscl  43831  lincellss  43882
  Copyright terms: Public domain W3C validator