Theorem ssexg 4251

Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
ssexg	|- ( ( A C_ B /\ B e. C ) -> A e. _V )

Proof of Theorem ssexg

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq2 3264	. . . 4 |- ( x = B -> ( A C_ x <-> A C_ B ) )
2	1	imbi1d 231	. . 3 |- ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3		vex 2818	. . . 4 |- x e. _V
4	3	ssex 4249	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2877	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 125	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2205   _Vcvv 2815   C_ wss 3213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4230

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-in 3219  df-ss 3226

This theorem is referenced by:  ssexd  4252  prcssprc  4253  difexg  4254  rabexg  4257  elssabg  4262  elpw2g  4270  abssexg  4297  snexg  4299  sess1  4460  sess2  4461  trsuc  4545  unexb  4565  abnexg  4569  uniexb  4596  xpexg  4866  riinint  5020  dmexg  5023  rnexg  5024  resexg  5080  resiexg  5085  imaexg  5117  exse2  5138  cnvexg  5302  coexg  5309  fabexg  5556  f1oabexg  5628  relrnfvex  5690  fvexg  5691  sefvex  5693  mptfvex  5765  mptexg  5913  ofres  6283  resfunexgALT  6303  cofunexg  6304  fnexALT  6306  f1dmex  6311  oprabexd  6322  mpoexxg  6408  suppfnss  6459  tposexg  6491  frecabex  6631  erex  6793  mapex  6890  pmvalg  6895  elpmg  6900  elmapssres  6909  pmss12g  6911  ixpexgg  6959  ssdomg  7020  fiprc  7059  fival  7259  iccen  10343  wrdexb  11240  shftfvalg  11507  shftfval  11510  tgval  13492  tgvalex  13493  toponsspwpwg  14904  eltg  14934  eltg2  14935  tgss  14945  basgen2  14963  bastop1  14965  topnex  14968  resttopon  15053  restabs  15057  lmfval  15075  cnrest  15117  txss12  15148  metrest  15388  dvbss  15567  dvcnp2cntop  15581  dvaddxxbr  15583  dvmulxxbr  15584  elply2  15617  plyf  15619  plyss  15620  elplyr  15622  plyaddlem  15631  plymullem  15632  plyco  15641  clwwlkex  16410