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

Theorem ssexg 3492
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 3490 . . 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 3493  rabexg 3495  elssabg 3497  elpw2g 3498  abssexg 3524  snexALT 3525  trsuc 3777  ordsssuc2 3782  unexb 3819  difex2 3824  uniexb 3878  xpexg 4122  dmexg 4232  rnexg 4233  resexg 4276  resiexg 4279  imaexg 4304  cnvexg 4443  coexg 4449  fabexg 4590  f1oabexg 4644  resfunexgALT 4789  cofunexg 4790  fnexALT 4793  opabex2g 4797  f1dmex 4803  oprabexd 4991  oprabex2g 4993  tz7.48-3 5345  oaabs 5485  mapex 5586  pmvalg 5590  elpmg 5593  pmss12g 5598  ixpexg 5627  ssdom2g 5683  fiprc 5710  infensuc 5843  pssnn 5884  fival 5942  fiss 5951  wofib 5994  card2on 5996  tcss 6070  aceq8alem 6301  cdainflem 6360  cfslb 6388  cofsmo 6391  inar1 6630  gruen 6663  shftfval 8787  summolem2 9160  islbs2 10342  issubg 10516  istps3OLD 10709  istps3 10714  tgval 10732  eltg 10734  eltg2 10735  basgen2 10757  subspval 10868  stoig2 10873  stoig 10874  subcld 10880  lpval 10886  cnsubsp 10924  cnsubsp2 10925  cmpcov 10947  cmpsublem 10948  cmpsub 10949  connsub 10962  cnmpt2res 10998  homeofval 11004  isfil2 11036  isfildlem 11037  infil 11044  flimfval 11065  subtopmet 11199  cnmptre 11280  lmfval 11354  metelcls 11400  metcld2 11402  cmsss 11411  bcthlem1 11413  elply2 13523  plyf 13525  plyss 13526  elplyr 13528  plyeq0lem 13535  plyeq0 13536  plyaddlem 13544  plymullem 13545  dgrlem 13555  coeidlem 13563  ovoliunlem1 13636  dfon2lem3 13994  setlikess 14063  tz6.26 14075  frmin 14111  altxpexg 14387  oprabex2gpop 14928  prjmapcp 15090  prjmapcp2 15096  ubpar 15181  qusp 15500  fgsb2 15513  cnfilca 15514  trfil 15521  islimrs3 15547  islimrs4 15548  consuba 15725  uncon 15731  dualded 15810  dualcat2 15811  elincin 15904  tarax3a 15906  tarax3c 15908  fnctartar3 15959  prismorcsetlem 15962  prismorcset 15964  domcatfun 15976  codcatfun 15985  isline1 16036  lemindclsbu 16081  indcls2 16082  cncls 16204  subsubtop 16208  subcls 16209  subntr 16210  ivthALT 16228  topjoin 16301  fnejoin1 16304  filssufil 16348  flimcls 16364  rnelfmlem 16368  rnelfm 16369  fmfnfmlem4 16373  sfcls 16380  filnetlem3 16418  filnetlem4 16419  abrexdom 16497  sdclem2 16550  sdclem1 16551  cnres2 16581  cnresima 16582  cnss 16583  sstotbnd 16597  totbndss 16598  ismtyval 16608  erex 16825  bnj74 17724  bnj1412 18795
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 3472
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