Theorem ssexi 4172

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 4171	. 2 |- ( A C_ B -> A e. _V )
4	1, 3	ax-mp 5	1 |- A e. _V

Syntax hints:   e. wcel 2167   _Vcvv 2763   C_ wss 3157

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  zfausab  4176  pp0ex  4223  ord3ex  4224  epse  4378  opabex  5789  mptexw  6179  oprabex  6194  mpoexw  6280  phplem2  6923  phpm  6935  snexxph  7025  sbthlem2  7033  2omotaplemst  7341  niex  7396  enqex  7444  enq0ex  7523  npex  7557  ltnqex  7633  gtnqex  7634  recexprlemell  7706  recexprlemelu  7707  enrex  7821  axcnex  7943  peano5nnnn  7976  reex  8030  nnex  9013  zex  9352  qex  9723  ixxex  9991  iccen  10098  serclim0  11487  climle  11516  iserabs  11657  isumshft  11672  explecnv  11687  prodfclim1  11726  prmex  12306  exmidunben  12668  prdsex  12971  prdsval  12975  fngsum  13090  igsumvalx  13091  metuex  14187  cnfldstr  14190  cnfldle  14199  znval  14268  znle  14269  znbaslemnn  14271  istopon  14333  dmtopon  14343  lmres  14568  climcncf  14904  reldvg  14999