HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ssexg 3489
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized).
Assertion
Ref Expression
ssexg |- ((A C_ B /\ B e. C) -> A e. _V)

Proof of Theorem ssexg
StepHypRef Expression
1 sseq2 2700 . . . 4 |- (x = B -> (A C_ x <-> A C_ B))
21imbi1d 321 . . 3 |- (x = B -> ((A C_ x -> A e. _V) <-> (A C_ B -> A e. _V)))
3 vex 2361 . . . 4 |- x e. _V
43ssex 3487 . . 3 |- (A C_ x -> A e. _V)
52, 4vtoclg 2409 . 2 |- (B e. C -> (A C_ B -> A e. _V))
65impcom 438 1 |- ((A C_ B /\ B e. C) -> A e. _V)
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 377   = wceq 1449   e. wcel 1451  _Vcvv 2358   C_ wss 2657
This theorem is referenced by:  difexg 3490  rabexg 3492  elssabg 3494  elpw2g 3495  abssexg 3521  snexALT 3522  trsuc 3774  ordsssuc2 3779  unexb 3816  difex2 3821  uniexb 3882  xpexg 4126  dmexg 4236  rnexg 4237  resexg 4281  resiexg 4284  imaexg 4309  cnvexg 4448  coexg 4454  fabexg 4595  f1oabexg 4650  resfunexgALT 4796  cofunexg 4797  fnexALT 4800  opabex2g 4804  f1dmex 4810  oprabexd 4998  oprabex2g 5000  tz7.48-3 5381  oaabs 5521  mapex 5622  pmvalg 5626  elpmg 5629  pmss12g 5634  ixpexg 5663  ssdom2g 5719  fiprc 5746  infensuc 5879  pssnn 5920  fival 5979  fiss 5988  wofib 6032  card2on 6034  tcss 6108  aceq8alem 6339  cdainflem 6398  cfslb 6426  cofsmo 6429  inar1 6668  gruen 6701  shftfval 8838  summolem2 9226  islbs2 10427  issubg 10614  istps3OLD 10807  istps3 10812  tgval 10830  eltg 10832  eltg2 10833  basgen2 10855  subspval 10967  stoig2 10972  stoig 10973  subsubtop 10975  subcld 10980  subcls 10983  subntr 10984  lpval 10988  cnsubsp 11026  cnsubsp2 11027  cnpsubsp 11029  cnpsubsp2 11030  cmpcov 11051  cmpsublem 11052  cmpsub 11053  connsub 11066  cnmpt2res 11105  homeofval 11111  isfil2 11143  isfildlem 11144  infil 11151  flimfval 11172  subtopmet 11306  cnmptre 11392  bndth 11410  lmfval 11468  metelcls 11514  metcld2 11516  cmsss 11525  bcthlem1 11527  ovoliunlem1 12016  mbfimaopn2 12129  cncombf 12130  0pledm 12145  dvfval 12336  dvlmlem2 12343  dvreslem 12347  dvcnp2 12353  dvcn 12354  dvaddbr 12355  dvmulbr 12356  dvadd 12357  dvmul 12358  dvaddf 12359  dvmulf 12360  dvcmulf 12362  dvcobr 12363  dvcof 12365  dvcjbr 12366  dvmptadd 12375  dvmptmul 12376  dvmptco 12386  ftc1lemf 12395  elply2 12419  plyf 12421  plyss 12422  elplyr 12424  plyeq0lem 12433  plyeq0 12434  plyaddlem 12437  plymullem 12438  dgrlem 12451  coeidlem 12459  dfon2lem3 14514  setlikess 14583  tz6.26 14595  frmin 14631  altxpexg 14907  oprabex2gpop 15448  prjmapcp 15609  prjmapcp2 15615  ubpar 15700  qusp 16016  fgsb2 16029  cnfilca 16030  trfil 16037  islimrs3 16063  islimrs4 16064  consuba 16241  uncon 16247  dualded 16326  dualcat2 16327  elincin 16420  tarax3a 16422  tarax3c 16424  fnctartar3 16475  prismorcsetlem 16478  prismorcset 16480  domcatfun 16492  codcatfun 16501  isline1 16552  lemindclsbu 16597  indcls2 16598  cncls 16716  ivthALT 16737  topjoin 16810  fnejoin1 16813  filssufil 16857  flimcls 16873  rnelfmlem 16877  rnelfm 16878  fmfnfmlem4 16882  sfcls 16889  filnetlem3 16927  filnetlem4 16928  abrexdom 17006  sdclem2 17058  sdclem1 17059  cnres2 17089  cnresima 17090  cnss 17091  sstotbnd 17105  totbndss 17106  ismtyval 17116  erex 17333  bnj74 18232  bnj1412 19303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-sep 3469
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-ex 1372  df-sb 1626  df-clab 1941  df-cleq 1946  df-clel 1949  df-v 2360  df-in 2664  df-ss 2666
Copyright terms: Public domain