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

Theorem ssexg 3494
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 2705 . . . 4 |- (x = B -> (A C_ x <-> A C_ B))
21imbi1d 326 . . 3 |- (x = B -> ((A C_ x -> A e. _V) <-> (A C_ B -> A e. _V)))
3 vex 2368 . . . 4 |- x e. _V
43ssex 3492 . . 3 |- (A C_ x -> A e. _V)
52, 4vtoclg 2416 . 2 |- (B e. C -> (A C_ B -> A e. _V))
65impcom 444 1 |- ((A C_ B /\ B e. C) -> A e. _V)
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 382   = wceq 1457   e. wcel 1459  _Vcvv 2365   C_ wss 2662
This theorem is referenced by:  difexg 3495  rabexg 3497  elssabg 3499  elpw2g 3500  abssexg 3526  snexALT 3527  trsuc 3779  ordsssuc2 3784  unexb 3821  difex2 3826  uniexb 3880  xpexg 4124  dmexg 4234  rnexg 4235  resexg 4279  resiexg 4282  imaexg 4307  cnvexg 4446  coexg 4452  fabexg 4593  f1oabexg 4648  resfunexgALT 4794  cofunexg 4795  fnexALT 4798  opabex2g 4802  f1dmex 4808  oprabexd 4996  oprabex2g 4998  tz7.48-3 5351  oaabs 5491  mapex 5592  pmvalg 5596  elpmg 5599  pmss12g 5604  ixpexg 5633  ssdom2g 5689  fiprc 5716  infensuc 5849  pssnn 5890  fival 5948  fiss 5957  wofib 6000  card2on 6002  tcss 6076  aceq8alem 6307  cdainflem 6366  cfslb 6394  cofsmo 6397  inar1 6636  gruen 6669  shftfval 8797  summolem2 9172  islbs2 10360  issubg 10536  istps3OLD 10729  istps3 10734  tgval 10752  eltg 10754  eltg2 10755  basgen2 10777  subspval 10889  stoig2 10894  stoig 10895  subsubtop 10897  subcld 10902  subcls 10905  subntr 10906  lpval 10910  cnsubsp 10948  cnsubsp2 10949  cnpsubsp 10951  cnpsubsp2 10952  cmpcov 10973  cmpsublem 10974  cmpsub 10975  connsub 10988  cnmpt2res 11025  homeofval 11031  isfil2 11063  isfildlem 11064  infil 11071  flimfval 11092  subtopmet 11226  cnmptre 11309  lmfval 11383  metelcls 11429  metcld2 11431  cmsss 11440  bcthlem1 11442  elply2 13625  plyf 13627  plyss 13628  elplyr 13630  plyeq0lem 13640  plyeq0 13641  plyaddlem 13644  plymullem 13645  dgrlem 13658  coeidlem 13666  ovoliunlem1 13804  0pledm 13894  dvfval 13987  dvlmlem2 13993  dvreslem 13997  dvcnp2 14003  dvaddbr 14004  dvmulbr 14005  dvadd 14006  dvmul 14007  dvaddf 14008  dvmulf 14009  dvcmulf 14011  dvcobr 14012  dvcof 14014  dfon2lem3 14215  setlikess 14284  tz6.26 14296  frmin 14332  altxpexg 14608  oprabex2gpop 15149  prjmapcp 15310  prjmapcp2 15316  ubpar 15401  qusp 15717  fgsb2 15730  cnfilca 15731  trfil 15738  islimrs3 15764  islimrs4 15765  consuba 15942  uncon 15948  dualded 16027  dualcat2 16028  elincin 16121  tarax3a 16123  tarax3c 16125  fnctartar3 16176  prismorcsetlem 16179  prismorcset 16181  domcatfun 16193  codcatfun 16202  isline1 16253  lemindclsbu 16298  indcls2 16299  cncls 16418  ivthALT 16439  topjoin 16512  fnejoin1 16515  filssufil 16559  flimcls 16575  rnelfmlem 16579  rnelfm 16580  fmfnfmlem4 16584  sfcls 16591  filnetlem3 16629  filnetlem4 16630  abrexdom 16708  sdclem2 16761  sdclem1 16762  cnres2 16792  cnresima 16793  cnss 16794  sstotbnd 16808  totbndss 16809  ismtyval 16819  erex 17036  bnj74 17935  bnj1412 19006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-sep 3474
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-ex 1381  df-sb 1633  df-clab 1948  df-cleq 1953  df-clel 1956  df-v 2367  df-in 2669  df-ss 2671
Copyright terms: Public domain