Theorem ssexg 4228

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 3251	. . . 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 2805	. . . 4 |- x e. _V
4	3	ssex 4226	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2864	. 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 1397   e. wcel 2202   _Vcvv 2802   C_ wss 3200

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206  df-ss 3213

This theorem is referenced by:  ssexd  4229  prcssprc  4230  difexg  4231  rabexg  4233  elssabg  4238  elpw2g  4246  abssexg  4272  snexg  4274  sess1  4434  sess2  4435  trsuc  4519  unexb  4539  abnexg  4543  uniexb  4570  xpexg  4840  riinint  4993  dmexg  4996  rnexg  4997  resexg  5053  resiexg  5058  imaexg  5090  exse2  5110  cnvexg  5274  coexg  5281  fabexg  5524  f1oabexg  5595  relrnfvex  5657  fvexg  5658  sefvex  5660  mptfvex  5732  mptexg  5879  ofres  6250  resfunexgALT  6270  cofunexg  6271  fnexALT  6273  f1dmex  6278  oprabexd  6289  mpoexxg  6375  tposexg  6424  frecabex  6564  erex  6726  mapex  6823  pmvalg  6828  elpmg  6833  elmapssres  6842  pmss12g  6844  ixpexgg  6891  ssdomg  6952  fiprc  6990  fival  7169  iccen  10241  wrdexb  11129  shftfvalg  11396  shftfval  11399  tgval  13363  tgvalex  13364  toponsspwpwg  14765  eltg  14795  eltg2  14796  tgss  14806  basgen2  14824  bastop1  14826  topnex  14829  resttopon  14914  restabs  14918  lmfval  14936  cnrest  14978  txss12  15009  metrest  15249  dvbss  15428  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  elply2  15478  plyf  15480  plyss  15481  elplyr  15483  plyaddlem  15492  plymullem  15493  plyco  15502  clwwlkex  16268