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

Theorem ssexg 3495
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 2706 . . . 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 2369 . . . 4 |- x e. _V
43ssex 3493 . . 3 |- (A C_ x -> A e. _V)
52, 4vtoclg 2417 . 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 2366   C_ wss 2663
This theorem is referenced by:  difexg 3496  rabexg 3498  elssabg 3500  elpw2g 3501  abssexg 3527  snexALT 3528  trsuc 3780  ordsssuc2 3785  unexb 3822  difex2 3827  uniexb 3886  xpexg 4130  dmexg 4240  rnexg 4241  resexg 4285  resiexg 4288  imaexg 4313  cnvexg 4452  coexg 4458  fabexg 4599  f1oabexg 4654  resfunexgALT 4800  cofunexg 4801  fnexALT 4804  opabex2g 4808  f1dmex 4814  oprabexd 5002  oprabex2g 5004  tz7.48-3 5384  oaabs 5524  mapex 5625  pmvalg 5629  elpmg 5632  pmss12g 5637  ixpexg 5666  ssdom2g 5722  fiprc 5749  infensuc 5882  pssnn 5923  fival 5981  fiss 5990  wofib 6033  card2on 6035  tcss 6109  aceq8alem 6340  cdainflem 6399  cfslb 6427  cofsmo 6430  inar1 6669  gruen 6702  shftfval 8834  summolem2 9210  islbs2 10376  issubg 10552  istps3OLD 10745  istps3 10750  tgval 10768  eltg 10770  eltg2 10771  basgen2 10793  subspval 10905  stoig2 10910  stoig 10911  subsubtop 10913  subcld 10918  subcls 10921  subntr 10922  lpval 10926  cnsubsp 10964  cnsubsp2 10965  cnpsubsp 10967  cnpsubsp2 10968  cmpcov 10989  cmpsublem 10990  cmpsub 10991  connsub 11004  cnmpt2res 11041  homeofval 11047  isfil2 11079  isfildlem 11080  infil 11087  flimfval 11108  subtopmet 11242  cnmptre 11327  bndth 11345  lmfval 11403  metelcls 11449  metcld2 11451  cmsss 11460  bcthlem1 11462  ovoliunlem1 11946  0pledm 12058  dvfval 12213  dvlmlem2 12219  dvreslem 12223  dvcnp2 12229  dvaddbr 12230  dvmulbr 12231  dvadd 12232  dvmul 12233  dvaddf 12234  dvmulf 12235  dvcmulf 12237  dvcobr 12238  dvcof 12240  elply2 12256  plyf 12258  plyss 12259  elplyr 12261  plyeq0lem 12270  plyeq0 12271  plyaddlem 12274  plymullem 12275  dgrlem 12288  coeidlem 12296  dfon2lem3 14317  setlikess 14386  tz6.26 14398  frmin 14434  altxpexg 14710  oprabex2gpop 15251  prjmapcp 15412  prjmapcp2 15418  ubpar 15503  qusp 15819  fgsb2 15832  cnfilca 15833  trfil 15840  islimrs3 15866  islimrs4 15867  consuba 16044  uncon 16050  dualded 16129  dualcat2 16130  elincin 16223  tarax3a 16225  tarax3c 16227  fnctartar3 16278  prismorcsetlem 16281  prismorcset 16283  domcatfun 16295  codcatfun 16304  isline1 16355  lemindclsbu 16400  indcls2 16401  cncls 16520  ivthALT 16541  topjoin 16614  fnejoin1 16617  filssufil 16661  flimcls 16677  rnelfmlem 16681  rnelfm 16682  fmfnfmlem4 16686  sfcls 16693  filnetlem3 16731  filnetlem4 16732  abrexdom 16810  sdclem2 16863  sdclem1 16864  cnres2 16894  cnresima 16895  cnss 16896  sstotbnd 16910  totbndss 16911  ismtyval 16921  erex 17138  bnj74 18037  bnj1412 19108
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 1672  ax-ext 1943  ax-sep 3475
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-ex 1381  df-sb 1634  df-clab 1949  df-cleq 1954  df-clel 1957  df-v 2368  df-in 2670  df-ss 2672
Copyright terms: Public domain