Theorem ssexi 2715

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 2714	. 2 |- (A (_ B -> A e. V)
4	1, 3	ax-mp 7	1 |- A e. V

Syntax hints:   e. wcel 956  Vcvv 1807   (_ wss 2043

This theorem is referenced by:  zfausab 2718  snex 2745  moabex 2761  opabex 3601  fvclex 3847  abrexexlem1 3849  abrexex 3851  oprabex 4010  pw2en 4432  sbthlem2 4434  phplem2 4495  phplem4 4497  php 4499  pssnn 4519  abfii2 4542  abfii4 4544  inf3lem3 4595  hta 4708  aceq3 4713  aceq5lem4 4718  aceq6b 4722  numthlem 4763  zorn2lem1 4768  brdom7disj 4784  brdom6disj 4785  niex 4989  enqex 5028  npex 5071  enrex 5158  reex 5292  nnex 5889  nn0ex 6060  zex 6099  qex 6214  sumex 6927  infxpidmlem9 7511  infmap2lem2 7530  gch-kn 7537  subbas 7594  bcthlem15 7963  issubg 8068  issubgi 8074  sspval 8329  ajfval 8413  shex 9016  chex 9034  hmopex 9742

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049

Copyright terms: Public domain