Theorem ssexi 1701

Description: The subset of a set is also a set.

Hypotheses

Ref	Expression
ssexi.1	|- B e. V
ssexi.2	|- A (_ B

Assertion

Ref	Expression
ssexi	|- A e. V

Proof of Theorem ssexi

Step	Hyp	Ref	Expression
1		ssexi.2	. 2 |- A (_ B
2		ssexi.1	. . 3 |- B e. V
3	2	ssex 1700	. 2 |- (A (_ B -> A e. V)
4	1, 3	ax-mp 6	1 |- A e. V

Syntax hints:   e. wcel 1092  Vcvv 1348   (_ wss 1487

This theorem is referenced by:  zfausab 1704  snex 1859  moabex 1868  xpex 2488  funopabex 2742  fvclex 2908  abrexexlem1 2910  abrexex 2912  oprabex 3044  qsex 3231  pw2en 3348  sbthlem2 3350  phplem3 3405  phplem5 3407  php 3409  pssnn 3428  inf3lem3 3466  aceq3 3556  aceq5lem4 3561  aceq6b 3565  numthlem 3598  zornlem1 3603  hta 3619  niex 3803  enqex 3842  npex 3885  enrex 3972  nnssre 4425  nnex 4431  nn0ex 4540  zex 4571  reex 4640  qex 4641  revalt 4794  imvalt 4795  infxpidmlem9 4941  infmap2lem2 4952  gch-kn 4957  shex 5115  chex 5130

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-in 1491  df-ss 1492

metamath.org