Theorem ssexi 4183

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

Syntax hints:   ∈ wcel 2176  Vcvv 2772   ⊆ wss 3166

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  zfausab  4187  pp0ex  4234  ord3ex  4235  epse  4390  opabex  5810  mptexw  6200  oprabex  6215  mpoexw  6301  phplem2  6952  phpm  6964  snexxph  7054  sbthlem2  7062  2omotaplemst  7372  niex  7427  enqex  7475  enq0ex  7554  npex  7588  ltnqex  7664  gtnqex  7665  recexprlemell  7737  recexprlemelu  7738  enrex  7852  axcnex  7974  peano5nnnn  8007  reex  8061  nnex  9044  zex  9383  qex  9755  ixxex  10023  iccen  10130  serclim0  11649  climle  11678  iserabs  11819  isumshft  11834  explecnv  11849  prodfclim1  11888  prmex  12468  exmidunben  12830  prdsex  13134  prdsval  13138  fngsum  13253  igsumvalx  13254  metuex  14350  cnfldstr  14353  cnfldle  14362  znval  14431  znle  14432  znbaslemnn  14434  istopon  14518  dmtopon  14528  lmres  14753  climcncf  15089  reldvg  15184