Theorem ssexi 4227

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

Syntax hints:   ∈ wcel 2202  Vcvv 2802   ⊆ wss 3200

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206  df-ss 3213

This theorem is referenced by:  zfausab  4232  pp0ex  4279  ord3ex  4280  epse  4439  opabex  5878  mptexw  6275  oprabex  6290  mpoexw  6378  phplem2  7039  phpm  7052  snexxph  7149  sbthlem2  7157  2omotaplemst  7477  niex  7532  enqex  7580  enq0ex  7659  npex  7693  ltnqex  7769  gtnqex  7770  recexprlemell  7842  recexprlemelu  7843  enrex  7957  axcnex  8079  peano5nnnn  8112  reex  8166  nnex  9149  zex  9488  qex  9866  ixxex  10134  iccen  10241  serclim0  11883  climle  11912  iserabs  12054  isumshft  12069  explecnv  12084  prodfclim1  12123  prmex  12703  exmidunben  13065  prdsex  13370  prdsval  13374  fngsum  13489  igsumvalx  13490  metuex  14588  cnfldstr  14591  cnfldle  14600  znval  14669  znle  14670  znbaslemnn  14672  istopon  14756  dmtopon  14766  lmres  14991  climcncf  15327  reldvg  15422