Theorem ssexg 4144

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 3181	. . . 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 2742	. . . 4 |- x e. _V
4	3	ssex 4142	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2799	. 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 1353   e. wcel 2148   _Vcvv 2739   C_ wss 3131

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4123

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-in 3137  df-ss 3144

This theorem is referenced by:  ssexd  4145  difexg  4146  rabexg  4148  elssabg  4150  elpw2g  4158  abssexg  4184  snexg  4186  sess1  4339  sess2  4340  trsuc  4424  unexb  4444  abnexg  4448  uniexb  4475  xpexg  4742  riinint  4890  dmexg  4893  rnexg  4894  resexg  4949  resiexg  4954  imaexg  4984  exse2  5004  cnvexg  5168  coexg  5175  fabexg  5405  f1oabexg  5475  relrnfvex  5535  fvexg  5536  sefvex  5538  mptfvex  5603  mptexg  5743  ofres  6099  resfunexgALT  6111  cofunexg  6112  fnexALT  6114  f1dmex  6119  oprabexd  6130  mpoexxg  6213  tposexg  6261  frecabex  6401  erex  6561  mapex  6656  pmvalg  6661  elpmg  6666  elmapssres  6675  pmss12g  6677  ixpexgg  6724  ssdomg  6780  fiprc  6817  fival  6971  iccen  10008  shftfvalg  10829  shftfval  10832  tgval  12716  tgvalex  12717  toponsspwpwg  13607  eltg  13637  eltg2  13638  tgss  13648  basgen2  13666  bastop1  13668  topnex  13671  resttopon  13756  restabs  13760  lmfval  13777  cnrest  13820  txss12  13851  metrest  14091  dvbss  14239  dvcnp2cntop  14248  dvaddxxbr  14250  dvmulxxbr  14251