Theorem ssexg 4173

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 3208	. . . 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 2766	. . . 4 |- x e. _V
4	3	ssex 4171	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2824	. 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 1364   e. wcel 2167   _Vcvv 2763   C_ wss 3157

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  ssexd  4174  difexg  4175  rabexg  4177  elssabg  4182  elpw2g  4190  abssexg  4216  snexg  4218  sess1  4373  sess2  4374  trsuc  4458  unexb  4478  abnexg  4482  uniexb  4509  xpexg  4778  riinint  4928  dmexg  4931  rnexg  4932  resexg  4987  resiexg  4992  imaexg  5024  exse2  5044  cnvexg  5208  coexg  5215  fabexg  5446  f1oabexg  5517  relrnfvex  5577  fvexg  5578  sefvex  5580  mptfvex  5648  mptexg  5788  ofres  6151  resfunexgALT  6166  cofunexg  6167  fnexALT  6169  f1dmex  6174  oprabexd  6185  mpoexxg  6269  tposexg  6317  frecabex  6457  erex  6617  mapex  6714  pmvalg  6719  elpmg  6724  elmapssres  6733  pmss12g  6735  ixpexgg  6782  ssdomg  6838  fiprc  6875  fival  7037  iccen  10083  wrdexb  10949  shftfvalg  10985  shftfval  10988  tgval  12943  tgvalex  12944  toponsspwpwg  14268  eltg  14298  eltg2  14299  tgss  14309  basgen2  14327  bastop1  14329  topnex  14332  resttopon  14417  restabs  14421  lmfval  14438  cnrest  14481  txss12  14512  metrest  14752  dvbss  14931  dvcnp2cntop  14945  dvaddxxbr  14947  dvmulxxbr  14948  elply2  14981  plyf  14983  plyss  14984  elplyr  14986  plyaddlem  14995  plymullem  14996  plyco  15005