Theorem ssexi 4142

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

Hypotheses

Ref	Expression
ssexi.1	⊢ 𝐵 ∈ V
ssexi.2	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
ssexi	⊢ 𝐴 ∈ V

Proof of Theorem ssexi

Step	Hyp	Ref	Expression
1		ssexi.2	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssexi.1	. . 3 ⊢ 𝐵 ∈ V
3	2	ssex 4141	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
4	1, 3	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2148  Vcvv 2738   ⊆ wss 3130

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 4122

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 2740  df-in 3136  df-ss 3143

This theorem is referenced by:  zfausab  4146  pp0ex  4190  ord3ex  4191  epse  4343  opabex  5741  mptexw  6114  oprabex  6129  mpoexw  6214  phplem2  6853  phpm  6865  snexxph  6949  sbthlem2  6957  2omotaplemst  7257  niex  7311  enqex  7359  enq0ex  7438  npex  7472  ltnqex  7548  gtnqex  7549  recexprlemell  7621  recexprlemelu  7622  enrex  7736  axcnex  7858  peano5nnnn  7891  reex  7945  nnex  8925  zex  9262  qex  9632  ixxex  9899  iccen  10006  serclim0  11313  climle  11342  iserabs  11483  isumshft  11498  explecnv  11513  prodfclim1  11552  prmex  12113  exmidunben  12427  prdsex  12718  istopon  13516  dmtopon  13526  lmres  13751  climcncf  14074  reldvg  14151