Theorem ssexi 4125

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 4124	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
4	1, 3	ax-mp 5	1 ⊢ 𝐴 ∈ V

Syntax hints:   ∈ wcel 2141  Vcvv 2730   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  zfausab  4129  pp0ex  4173  ord3ex  4174  epse  4325  opabex  5718  mptexw  6090  oprabex  6105  mpoexw  6190  phplem2  6829  phpm  6841  snexxph  6925  sbthlem2  6933  niex  7267  enqex  7315  enq0ex  7394  npex  7428  ltnqex  7504  gtnqex  7505  recexprlemell  7577  recexprlemelu  7578  enrex  7692  axcnex  7814  peano5nnnn  7847  reex  7901  nnex  8877  zex  9214  qex  9584  ixxex  9849  iccen  9956  serclim0  11261  climle  11290  iserabs  11431  isumshft  11446  explecnv  11461  prodfclim1  11500  prmex  12060  exmidunben  12374  istopon  12770  dmtopon  12780  lmres  13007  climcncf  13330  reldvg  13407