Theorem ssexg 4267

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 3272	. . . 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 2824	. . . 4 |- x e. _V
4	3	ssex 4265	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2883	. 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 1402   e. wcel 2209   _Vcvv 2821   C_ wss 3220

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4244

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233

This theorem is referenced by:  ssexd  4268  prcssprc  4269  difexg  4270  rabexg  4274  elssabg  4279  elpw2g  4287  abssexg  4314  snexg  4316  sess1  4477  sess2  4478  trsuc  4562  unexb  4583  abnexg  4587  uniexb  4614  xpexg  4884  riinint  5038  dmexg  5041  rnexg  5042  resexg  5098  resiexg  5103  imaexg  5135  exse2  5156  cnvexg  5320  coexg  5327  fabexg  5574  f1oabexg  5646  relrnfvex  5708  fvexg  5709  sefvex  5711  mptfvex  5785  mptexg  5933  ofres  6307  resfunexgALT  6327  cofunexg  6328  fnexALT  6330  f1dmex  6335  oprabexd  6350  mpoexxg  6436  suppfnss  6487  tposexg  6519  frecabex  6659  erex  6821  mapex  6918  pmvalg  6923  elpmg  6928  elmapssres  6944  pmss12g  6946  ixpexgg  6994  ssdomg  7055  fiprc  7094  fival  7294  iccen  10388  wrdexb  11294  shftfvalg  11561  shftfval  11564  tgval  13593  tgvalex  13594  toponsspwpwg  15046  eltg  15076  eltg2  15077  tgss  15087  basgen2  15105  bastop1  15107  topnex  15110  resttopon  15195  restabs  15199  lmfval  15217  cnrest  15259  txss12  15290  metrest  15530  dvbss  15709  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  elply2  15759  plyf  15761  plyss  15762  elplyr  15764  plyaddlem  15773  plymullem  15774  plyco  15783  clwwlkex  16553