Theorem ssexg 3999

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 3063	. . . 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 2636	. . . 4 |- x e. _V
4	3	ssex 3997	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2693	. 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 1296   e. wcel 1445   _Vcvv 2633   C_ wss 3013

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-in 3019  df-ss 3026

This theorem is referenced by:  ssexd  4000  difexg  4001  rabexg  4003  elssabg  4005  elpw2g  4013  abssexg  4038  snexg  4040  sess1  4188  sess2  4189  trsuc  4273  unexb  4292  abnexg  4296  uniexb  4323  xpexg  4581  riinint  4726  dmexg  4729  rnexg  4730  resexg  4785  resiexg  4790  imaexg  4819  exse2  4839  cnvexg  5002  coexg  5009  fabexg  5233  f1oabexg  5300  relrnfvex  5358  fvexg  5359  sefvex  5361  mptfvex  5424  mptexg  5561  ofres  5907  resfunexgALT  5919  cofunexg  5920  fnexALT  5922  f1dmex  5925  oprabexd  5936  mpt2exxg  6015  tposexg  6061  frecabex  6201  erex  6356  mapex  6451  pmvalg  6456  elpmg  6461  elmapssres  6470  pmss12g  6472  ixpexgg  6519  ssdomg  6575  fiprc  6612  shftfvalg  10367  shftfval  10370  toponsspwpwg  11872  tgval  11901  tgvalex  11902  eltg  11904  eltg2  11905  tgss  11915  basgen2  11933  bastop1  11935  topnex  11938  resttopon  12023  restabs  12027  lmfval  12044  cnrest  12086  metrest  12292