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

Theorem ssexg 3478
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 2685 . . . 4 |- (x = B -> (A C_ x <-> A C_ B))
21imbi1d 308 . . 3 |- (x = B -> ((A C_ x -> A e. _V) <-> (A C_ B -> A e. _V)))
3 vex 2346 . . . 4 |- x e. _V
43ssex 3476 . . 3 |- (A C_ x -> A e. _V)
52, 4vtoclg 2394 . 2 |- (B e. C -> (A C_ B -> A e. _V))
65impcom 422 1 |- ((A C_ B /\ B e. C) -> A e. _V)
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 361   = wceq 1434   e. wcel 1436  _Vcvv 2343   C_ wss 2642
This theorem is referenced by:  difexg 3479  rabexg 3481  elssabg 3483  elpw2g 3484  abssexg 3510  snexALT 3511  trsuc 3765  ordsssuc2 3770  unexb 3807  difex2 3812  uniexb 3873  xpexg 4117  dmexg 4227  rnexg 4228  resexg 4272  resiexg 4275  imaexg 4300  cnvexg 4439  coexg 4445  fabexg 4586  f1oabexg 4641  resfunexgALT 4787  cofunexg 4788  fnexALT 4791  opabex2g 4795  f1dmex 4801  oprabexd 4989  oprabex2g 4991  ofres 5142  tz7.48-3 5374  oaabs 5514  mapex 5615  pmvalg 5619  elpmg 5622  pmss12g 5627  ixpexg 5656  ssdom2g 5712  fiprc 5739  infensuc 5872  pssnn 5913  fival 5972  fiss 5981  wofib 6025  card2on 6027  cdainflem 6381  cofsmo 6412  inar1 6651  gruen 6688  shftfval 8837  rlim 9125  o1of2 9191  o1rlimmul 9196  summolem2 9275  islbs2 10514  issubg 10703  istps3OLD 10897  istps3 10902  tgval 10920  eltg 10922  eltg2 10923  basgen2 10945  subspval 11057  stoig2 11062  stoig 11063  subsubtop 11065  subcld 11070  subcls 11073  subntr 11074  lpval 11078  cnsubsp 11116  cnsubsp2 11117  cnpsubsp 11119  cnpsubsp2 11120  cmpcov 11141  cmpsublem 11143  cmpsub 11144  connsub 11157  cnmpt2res 11200  homeofval 11206  hmeores 11213  isfil2 11239  isfildlem 11240  flimfval 11268  subtopmet 11402  cnmptre 11488  bndth 11506  lmfval 11564  metelcls 11610  metcld2 11612  cmsss 11621  bcthlem1 11623  cnheibor 12066  ovoliunlem1 12114  mbfimaopn2 12227  cncombf 12228  0pledm 12243  dvfval 12434  dvlmlem2 12441  dvreslem 12445  dvcnp2 12451  dvcn 12452  dvaddbr 12453  dvmulbr 12454  dvadd 12455  dvmul 12456  dvaddf 12457  dvmulf 12458  dvcmulf 12460  dvcobr 12461  dvcof 12463  dvcjbr 12464  dvmptadd 12473  dvmptmul 12474  dvmptco 12484  ftc1lemf 12493  elply2 12517  plyf 12519  plyss 12520  elplyr 12522  plyeq0lem 12531  plyeq0 12532  plyaddlem 12535  plymullem 12536  dgrlem 12549  coeidlem 12557  dfon2lem3 14706  setlikess 14775  tz6.26 14787  frmin 14823  altxpexg 15099  oprabex2gpop 15640  prjmapcp 15796  prjmapcp2 15802  ubpar 15887  qusp 16201  fgsb2 16214  cnfilca 16215  trfil 16222  islimrs3 16248  islimrs4 16249  consuba 16425  uncon 16431  dualded 16510  dualcat2 16511  fnctartar3 16631  prismorcsetlem 16634  prismorcset 16636  isline1 16708  lemindclsbu 16753  indcls2 16754  cncls 16872  ivthALT 16893  topjoin 16966  fnejoin1 16969  filssufil 17013  flimcls 17029  rnelfmlem 17033  rnelfm 17034  fmfnfmlem4 17038  sfcls 17045  filnetlem3 17083  filnetlem4 17084  abrexdom 17162  sdclem2 17212  sdclem1 17213  cnres2 17243  cnresima 17244  sstotbnd 17258  totbndss 17259  ismtyval 17269  erex 17485  bnj74 18383  bnj1412 19454
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-sep 3458
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-ex 1356  df-sb 1611  df-clab 1926  df-cleq 1931  df-clel 1934  df-v 2345  df-in 2649  df-ss 2651
Copyright terms: Public domain