Theorem ssexg 4075

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 3126	. . . 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 2692	. . . 4 |- x e. _V
4	3	ssex 4073	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2749	. 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 1332   e. wcel 1481   _Vcvv 2689   C_ wss 3076

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3082  df-ss 3089

This theorem is referenced by:  ssexd  4076  difexg  4077  rabexg  4079  elssabg  4081  elpw2g  4089  abssexg  4114  snexg  4116  sess1  4267  sess2  4268  trsuc  4352  unexb  4371  abnexg  4375  uniexb  4402  xpexg  4661  riinint  4808  dmexg  4811  rnexg  4812  resexg  4867  resiexg  4872  imaexg  4901  exse2  4921  cnvexg  5084  coexg  5091  fabexg  5318  f1oabexg  5387  relrnfvex  5447  fvexg  5448  sefvex  5450  mptfvex  5514  mptexg  5653  ofres  6004  resfunexgALT  6016  cofunexg  6017  fnexALT  6019  f1dmex  6022  oprabexd  6033  mpoexxg  6116  tposexg  6163  frecabex  6303  erex  6461  mapex  6556  pmvalg  6561  elpmg  6566  elmapssres  6575  pmss12g  6577  ixpexgg  6624  ssdomg  6680  fiprc  6717  fival  6866  iccen  9819  shftfvalg  10622  shftfval  10625  toponsspwpwg  12228  tgval  12257  tgvalex  12258  eltg  12260  eltg2  12261  tgss  12271  basgen2  12289  bastop1  12291  topnex  12294  resttopon  12379  restabs  12383  lmfval  12400  cnrest  12443  txss12  12474  metrest  12714  dvbss  12862  dvcnp2cntop  12871  dvaddxxbr  12873  dvmulxxbr  12874