HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ssexi 3494
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
StepHypRef Expression
1 ssexi.2 . 2 |- A C_ B
2 ssexi.1 . . 3 |- B e. _V
32ssex 3493 . 2 |- (A C_ B -> A e. _V)
41, 3ax-mp 8 1 |- A e. _V
Colors of variables: wff set class
Syntax hints:   e. wcel 1459  _Vcvv 2366   C_ wss 2663
This theorem is referenced by:  zfausab 3497  ord3ex 3532  moabex 3561  opabex 4806  fvclex 4873  abrexexlem1 4875  abrexex 4877  oprabex 5003  oev 5418  sbthlem2 5768  phplem2 5884  phplem4 5886  php 5888  pssnn 5923  ordtypelem1 6023  ordtypelem7 6029  hartogslem 6031  inf3lem3 6062  hta 6233  aceq3 6329  aceq5lem4 6334  aceq6b 6338  domtriomlem 6444  axdc3lem 6451  axcclem 6458  numthlem 6503  zorn2lem1 6508  brdom7disj 6528  brdom6disj 6529  unidom 6532  konigthlem 6558  infmap2lem2 6579  gch-kn 6586  niex 6765  enqex 6807  npex 6871  enrex 6954  isprm2lem 9651  1arithlem1 9788  1arith 9792  strss 9887  issubgi 10559  symgval 10644  cmpcld 10992  hmph 11054  blfval 11183  qtopbaslem 11264  divcn 11314  evth 11346  phtpyfval 11351  phtpcval 11358  pi1bval 11386  bcthlem1 11462  bcthlem5 11466  sspval 11671  ajfval 11759  vitalilem2 12006  vitalilem3 12007  vitali 12010  itg2seq 12119  shex 12859  chex 12874  hmopex 13524  dfon2lem7 14321  colinearex 14878  prodex 15554  issubcat 16190  isrocatset 16327  2ndcctbss 16565  neibastop2lem1 16606  neibastop2lem4 16609  heibor1lem 16930  heiborlem3 16934  rngohomval 16994  onfrALTlem3VD 17636  bnj20 18000  bnj53 18779  cmtfval 19211  cvrfval 19270  lineset 19793  psubspset 19799  psubclset 19992  lautset 20142  pautset 20163  tendoset 20893
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1672  ax-ext 1943  ax-sep 3475
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-ex 1381  df-sb 1634  df-clab 1949  df-cleq 1954  df-clel 1957  df-v 2368  df-in 2670  df-ss 2672
Copyright terms: Public domain