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  9299  iccen  10420  wrdexb  11332  shftfvalg  11599  shftfval  11602  tgval  13669  tgvalex  13670  toponsspwpwg  15214  eltg  15244  eltg2  15245  tgss  15255  basgen2  15273  bastop1  15275  topnex  15278  resttopon  15363  restabs  15367  lmfval  15385  cnrest  15427  txss12  15458  metrest  15698  dvbss  15877  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  elply2  15927  plyf  15929  plyss  15930  elplyr  15932  plyaddlem  15941  plymullem  15942  plyco  15951  clwwlkex  16805