Theorem ssexg 4233

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 3252	. . . 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 2806	. . . 4 |- x e. _V
4	3	ssex 4231	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2865	. 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 2202   _Vcvv 2803   C_ wss 3201

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 2213  ax-sep 4212

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207  df-ss 3214

This theorem is referenced by:  ssexd  4234  prcssprc  4235  difexg  4236  rabexg  4238  elssabg  4243  elpw2g  4251  abssexg  4278  snexg  4280  sess1  4440  sess2  4441  trsuc  4525  unexb  4545  abnexg  4549  uniexb  4576  xpexg  4846  riinint  4999  dmexg  5002  rnexg  5003  resexg  5059  resiexg  5064  imaexg  5096  exse2  5117  cnvexg  5281  coexg  5288  fabexg  5532  f1oabexg  5604  relrnfvex  5666  fvexg  5667  sefvex  5669  mptfvex  5741  mptexg  5889  ofres  6259  resfunexgALT  6279  cofunexg  6280  fnexALT  6282  f1dmex  6287  oprabexd  6298  mpoexxg  6384  suppfnss  6435  tposexg  6467  frecabex  6607  erex  6769  mapex  6866  pmvalg  6871  elpmg  6876  elmapssres  6885  pmss12g  6887  ixpexgg  6934  ssdomg  6995  fiprc  7033  fival  7229  iccen  10303  wrdexb  11191  shftfvalg  11458  shftfval  11461  tgval  13425  tgvalex  13426  toponsspwpwg  14833  eltg  14863  eltg2  14864  tgss  14874  basgen2  14892  bastop1  14894  topnex  14897  resttopon  14982  restabs  14986  lmfval  15004  cnrest  15046  txss12  15077  metrest  15317  dvbss  15496  dvcnp2cntop  15510  dvaddxxbr  15512  dvmulxxbr  15513  elply2  15546  plyf  15548  plyss  15549  elplyr  15551  plyaddlem  15560  plymullem  15561  plyco  15570  clwwlkex  16339