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

Theorem ssexg 3630
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 2842 . . . 4 |- (x = B -> (A C_ x <-> A C_ B))
21imbi1d 360 . . 3 |- (x = B -> ((A C_ x -> A e. _V) <-> (A C_ B -> A e. _V)))
3 visset 2502 . . . 4 |- x e. _V
43ssex 3628 . . 3 |- (A C_ x -> A e. _V)
52, 4vtoclg 2553 . 2 |- (B e. C -> (A C_ B -> A e. _V))
65impcom 481 1 |- ((A C_ B /\ B e. C) -> A e. _V)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 418   = wceq 1592   e. wcel 1594  _Vcvv 2499   C_ wss 2801
This theorem is referenced by:  difexg 3631  rabexg 3633  elssabg 3635  elpw2g 3636  abssexg 3662  snexALT 3663  trsuc 3913  ordsssuc2 3918  unexb 3955  difex2 3960  uniexb 4015  xpexg 4256  dmexg 4365  rnexg 4366  resexg 4409  resiexg 4412  imaexg 4437  cnvexg 4576  coexg 4582  fabexg 4731  f1oabexg 4785  resfunexgALT 4928  cofunexg 4929  fnexALT 4932  opabex2g 4936  f1dmex 4942  oprabexd 5134  oprabex2g 5136  tz7.48-3 5486  oaabs 5628  mapex 5709  pmvalg 5713  elpmg 5716  ixpexg 5741  ssdom2g 5797  fiprc 5825  infensuc 5960  pssnn 6001  fienf1f1o 6010  wofib 6098  card2on 6100  tcss 6177  aceq8alem 6448  cdainflem 6507  cfslb 6535  cofsmo 6538  inar1 6743  gruen 6776  shftfval 8675  istps3OLD 10407  istps3 10412  tgval 10430  eltg 10432  eltg2 10433  basgen2 10453  subspval 10580  stoig2 10585  stoig 10586  subcld 10592  lpval 10596  subtopmet 10742  lmfval 10785  lmbr 10788  metelcls 10826  bcthlem1 10862  fival 11690  fiss 11700  homeofval 11716  isfil2 11747  isfildlem 11748  infil 11755  flimfval 11775  sumnz 13547  dfon2lem3 14043  setlikess 14107  tz6.26 14117  frmin 14150  altxpexg 14356  oprabex2gpop 14824  prjmapcp 14992  prjmapcp2 15000  ubpar 15088  qusp 15416  fgsb2 15432  cnfilca 15433  trfil 15440  islimrs3 15466  islimrs4 15467  dualded 15691  dualcat2 15692  elincin 15784  tarax3a 15786  tarax3c 15788  fnctartar3 15839  prismorcsetlem 15842  prismorcset 15844  domcatfun 15856  codcatfun 15865  isline1 15916  lemindclsbu 15961  indcls2 15962  indclsbu 15965  indclsbu0 15966  indclsbusuc 15967  cncls 16093  subsubtop 16097  subcls 16098  subntr 16099  cnsubsp 16100  cnsubsp2 16101  compcov 16103  compsublem 16104  compsub 16105  connsub 16118  ivthALT 16129  topjoin 16202  fnejoin1 16205  filssufil 16249  flimcls 16265  rnelfmlem 16269  rnelfm 16270  fmfnfmlem4 16274  sfcls 16281  filnetlem3 16319  filnetlem4 16320  abrexdom 16412  sdclem2 16475  sdc 16476  cnimass 16552  cnres 16553  cnres2 16554  cnresima 16555  cnss 16556  tlmval 16567  sstotbnd 16600  totbndss 16601  ismtyval 16611  erex 16895  bnj74 17734  bnj1412 18805
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-sep 3609
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-ex 1521  df-sb 1765  df-clab 2080  df-cleq 2085  df-clel 2088  df-v 2501  df-in 2808  df-ss 2810
Copyright terms: Public domain