Theorem ssexg 4126

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 3171	. . . 4 |- ( x = B -> ( A C_ x <-> A C_ B ) )
2	1	imbi1d 230	. . 3 |- ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3		vex 2733	. . . 4 |- x e. _V
4	3	ssex 4124	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2790	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 124	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   e. wcel 2141   _Vcvv 2730   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  ssexd  4127  difexg  4128  rabexg  4130  elssabg  4132  elpw2g  4140  abssexg  4166  snexg  4168  sess1  4320  sess2  4321  trsuc  4405  unexb  4425  abnexg  4429  uniexb  4456  xpexg  4723  riinint  4870  dmexg  4873  rnexg  4874  resexg  4929  resiexg  4934  imaexg  4963  exse2  4983  cnvexg  5146  coexg  5153  fabexg  5383  f1oabexg  5452  relrnfvex  5512  fvexg  5513  sefvex  5515  mptfvex  5579  mptexg  5718  ofres  6072  resfunexgALT  6084  cofunexg  6085  fnexALT  6087  f1dmex  6092  oprabexd  6103  mpoexxg  6186  tposexg  6234  frecabex  6374  erex  6533  mapex  6628  pmvalg  6633  elpmg  6638  elmapssres  6647  pmss12g  6649  ixpexgg  6696  ssdomg  6752  fiprc  6789  fival  6943  iccen  9950  shftfvalg  10769  shftfval  10772  toponsspwpwg  12773  tgval  12802  tgvalex  12803  eltg  12805  eltg2  12806  tgss  12816  basgen2  12834  bastop1  12836  topnex  12839  resttopon  12924  restabs  12928  lmfval  12945  cnrest  12988  txss12  13019  metrest  13259  dvbss  13407  dvcnp2cntop  13416  dvaddxxbr  13418  dvmulxxbr  13419