Theorem ssexi 2720

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

Syntax hints:   e. wcel 958  Vcvv 1811   (_ wss 2047

This theorem is referenced by:  zfausab 2723  snex 2750  moabex 2766  opabex 3609  fvclex 3856  abrexexlem1 3858  abrexex 3860  oprabex 4019  pw2en 4446  sbthlem2 4448  phplem2 4509  phplem4 4511  php 4513  pssnn 4534  abfii2OLD 4562  abfii4OLD 4564  inf3lem3 4615  hta 4728  aceq3 4733  aceq5lem4 4738  aceq6b 4742  numthlem 4783  zorn2lem1 4788  brdom7disj 4804  brdom6disj 4805  niex 5009  enqex 5048  npex 5091  enrex 5178  reex 5312  nnex 5933  nn0ex 6105  zex 6144  qex 6268  sumex 6981  infxpidmlem9 7560  infmap2lem2 7580  gch-kn 7587  subbasOLD 7644  bcthlem15 8013  issubg 8116  issubgi 8122  sspval 8382  ajfval 8469  shex 9077  chex 9095  hmopex 9802

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-ss 2053

Copyright terms: Public domain