Theorem ssexi 3456

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

Hypotheses

Ref	Expression
ssexi.1	|- B e. _V
ssexi.2	|- A C_ B

Assertion

Ref	Expression
ssexi	|- A e. _V

Proof of Theorem ssexi

Step	Hyp	Ref	Expression
1		ssexi.2	. 2 |- A C_ B
2		ssexi.1	. . 3 |- B e. _V
3	2	ssex 3455	. 2 |- (A C_ B -> A e. _V)
4	1, 3	ax-mp 7	1 |- A e. _V

Syntax hints:   e. wcel 1300  _Vcvv 2292   C_ wss 2593

This theorem is referenced by:  zfausab 3459  snexOLD 3493  ord3ex 3497  moabex 3513  opabex 4538  fvclex 4832  abrexexlem1 4834  abrexex 4836  oprabex 4948  pw2en 5505  sbthlem2 5511  phplem2 5603  phplem4 5605  php 5607  pssnn 5628  abfii2 5652  abfii4 5654  ordtypelem1 5684  ordtypelem7 5690  hartog 5693  inf3lem3 5721  hta 5858  aceq3 5895  aceq5lem4 5900  aceq6b 5904  numthlem 5945  zorn2lem1 5950  brdom7disj 5966  brdom6disj 5967  niex 6161  enqex 6200  npex 6243  enrex 6330  reex 6465  nnex 7116  nn0ex 7314  zex 7353  qex 7448  sumex 8241  infxpidmlem9 8829  infmap2lem2 8849  gch-kn 8856  subbas 8914  bcthlem15 9291  issubg 9425  issubgi 9431  sspval 9721  ajfval 9809  stoiglem 10250  shex 10710  chex 10728  hmopex 11439  bnj20 12386  bnj53 13193  isprm2lem 13774  dfon2lem7 13855  prodex 14656  issubcat 15193  ordtypelem1OLD 15375  ordtypelem7OLD 15381  hartogOLD 15384  cptclsscpt 15432  2ndcctbss 15478  neibastop2lem1 15519  neibastop2lem4 15522  filssufil 15571  heiborlem23 15977  heiborlem25 15979  heiborlem26 15980  heiborlem29 15983  heiborlem40 15994  phtpcval 16058  pcofval 16072  pi1bval 16088  rnghomval 16118  cmtfval 16937  cvrfval 16987  csubspset 17208  lineset 17219  psubspset 17225  psubclset 17346  pautset 17395

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-in 2603  df-ss 2605

Copyright terms: Public domain