Theorem ssexg 4272

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 3272	. . . 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 2824	. . . 4 |- x e. _V
4	3	ssex 4270	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2883	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 125	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   _Vcvv 2821   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233

This theorem is used by:  ssexd  4273  prcssprc  4274  difexg  4275  rabexg  4279  elssabg  4284  elpw2g  4292  abssexg  4319  snexg  4321  sess1  4482  sess2  4483  trsuc  4567  unexb  4588  abnexg  4592  uniexb  4619  xpexg  4889  riinint  5043  dmexg  5046  rnexg  5047  resexg  5103  resiexg  5108  imaexg  5140  exse2  5161  cnvexg  5325  coexg  5332  fabexg  5579  f1oabexg  5651  relrnfvex  5713  fvexg  5714  sefvex  5716  mptfvex  5791  mptexg  5942  ofres  6317  resfunexgALT  6337  cofunexg  6338  fnexALT  6340  f1dmex  6345  oprabexd  6360  mpoexxg  6446  suppfnss  6497  tposexg  6529  frecabex  6669  erex  6831  mapex  6928  pmvalg  6933  elpmg  6938  elmapssres  6954  pmss12g  6956  ixpexgg  7004  ssdomg  7065  fiprc  7104  fival  7304  indval  9298  iccen  10419  wrdexb  11330  shftfvalg  11597  shftfval  11600  tgval  13665  tgvalex  13666  toponsspwpwg  15172  eltg  15202  eltg2  15203  tgss  15213  basgen2  15231  bastop1  15233  topnex  15236  resttopon  15321  restabs  15325  lmfval  15343  cnrest  15385  txss12  15416  metrest  15656  dvbss  15835  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  elply2  15885  plyf  15887  plyss  15888  elplyr  15890  plyaddlem  15899  plymullem  15900  plyco  15909  clwwlkex  16737