Theorem ssexi 4225

Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)

Hypotheses

Ref	Expression
ssexi.1	|- B e. _V
ssexi.2	|- A C_ B

Assertion

Ref	Expression
ssexi	|- A e. _V

Proof of Theorem ssexi

Step	Hyp	Ref	Expression
1		ssexi.2	. 2 |- A C_ B
2		ssexi.1	. . 3 |- B e. _V
3	2	ssex 4224	. 2 |- ( A C_ B -> A e. _V )
4	1, 3	ax-mp 5	1 |- A e. _V

Syntax hints:   e. wcel 2200   _Vcvv 2800   C_ wss 3198

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-in 3204  df-ss 3211

This theorem is referenced by:  zfausab  4230  pp0ex  4277  ord3ex  4278  epse  4437  opabex  5873  mptexw  6270  oprabex  6285  mpoexw  6373  phplem2  7034  phpm  7047  snexxph  7140  sbthlem2  7148  2omotaplemst  7467  niex  7522  enqex  7570  enq0ex  7649  npex  7683  ltnqex  7759  gtnqex  7760  recexprlemell  7832  recexprlemelu  7833  enrex  7947  axcnex  8069  peano5nnnn  8102  reex  8156  nnex  9139  zex  9478  qex  9856  ixxex  10124  iccen  10231  serclim0  11856  climle  11885  iserabs  12026  isumshft  12041  explecnv  12056  prodfclim1  12095  prmex  12675  exmidunben  13037  prdsex  13342  prdsval  13346  fngsum  13461  igsumvalx  13462  metuex  14559  cnfldstr  14562  cnfldle  14571  znval  14640  znle  14641  znbaslemnn  14643  istopon  14727  dmtopon  14737  lmres  14962  climcncf  15298  reldvg  15393