Theorem ssexi 2794

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

Hypotheses

Ref	Expression
ssexi.1	⊢ B ∈ V
ssexi.2	⊢ A ⊆ B

Assertion

Ref	Expression
ssexi	⊢ A ∈ V

Proof of Theorem ssexi

Step	Hyp	Ref	Expression
1		ssexi.2	. 2 ⊢ A ⊆ B
2		ssexi.1	. . 3 ⊢ B ∈ V
3	2	ssex 2793	. 2 ⊢ (A ⊆ B → A ∈ V)
4	1, 3	ax-mp 7	1 ⊢ A ∈ V

Syntax hints:   ∈ wcel 994  Vcvv 1857   ⊆ wss 2099

This theorem is referenced by:  zfausab 2797  snex 2826  ord3ex 2830  moabex 2844  opabex 3715  fvclex 3970  abrexexlem1 3972  abrexex 3974  oprabex 4079  pw2en 4587  sbthlem2 4593  phplem2 4656  phplem4 4658  php 4660  pssnn 4681  abfii2 4705  abfii4 4707  inf3lem3 4760  hta 4874  aceq3 4879  aceq5lem4 4884  aceq6b 4888  numthlem 4929  zorn2lem1 4934  brdom7disj 4950  brdom6disj 4951  niex 5163  enqex 5202  npex 5245  enrex 5332  reex 5466  nnex 6078  nn0ex 6273  zex 6312  qex 6407  sumex 7184  infxpidmlem9 7772  infmap2lem2 7792  gch-kn 7799  subbas 7856  bcthlem15 8224  issubg 8358  issubgi 8364  sspval 8636  ajfval 8724  shex 9353  chex 9371  hmopex 10082  stoiglem 11063  issubcat 11299  ordtypelem1 11427  ordtypelem7 11433  hartog 11436  cptclsscpt 11489  2ndcctbss 11539  neibastop2lem1 11580  neibastop2lem4 11583  filssufil 11656  metsstop 11909  heiborlem23 12033  heiborlem25 12035  heiborlem26 12036  heiborlem29 12039  heiborlem40 12050  phtpcval 12100

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103  df-ss 2105

Copyright terms: Public domain