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

Theorem ssexi 3629
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 3628 . 2 |- (A C_ B -> A e. _V)
41, 3ax-mp 7 1 |- A e. _V
Colors of variables: wff set class
Syntax hints:   e. wcel 1594  _Vcvv 2499   C_ wss 2801
This theorem is referenced by:  zfausab 3632  ord3ex 3667  moabex 3695  opabex 4934  fvclex 5007  abrexexlem1 5009  abrexex 5011  oprabex 5135  oev 5522  pw2en 5841  sbthlem2 5843  phplem2 5962  phplem4 5964  php 5966  pssnn 6001  ordtypelem1 6088  ordtypelem7 6094  hartogslem 6096  inf3lem3 6127  hta 6340  aceq3 6437  aceq5lem4 6442  aceq6b 6446  domtriomlem 6552  axdc3lem 6559  axcclem 6566  numthlem 6611  zorn2lem1 6616  brdom7disj 6636  brdom6disj 6637  unidom 6640  konigthlem 6666  infmap2lem2 6687  gch-kn 6694  niex 6872  enqex 6914  npex 6978  enrex 7061  zex 8052  sumex 9169  isprm2lem 9898  strss 9966  subbas 10458  blfval 10684  bcthlem1 10862  bcthlem5 10866  issubg 10985  issubgi 10991  sspval 11276  ajfval 11364  symgval 11678  shex 12193  chex 12208  hmopex 12912  enrexNEW 13516  zexNEW 13585  dfon2lem7 14047  prodex 15141  issubcat 15752  isrocatset 15888  cptclsscpt 16106  2ndcctbss 16153  neibastop2lem1 16194  neibastop2lem4 16197  cnresoprab2 16580  heibor1lem 16620  heiborlem3 16624  phtpcval 16693  pcofval 16707  pi1bval 16723  rnghomval 16751  onfrALTlem3VD 17335  bnj20 17697  bnj53 18476  cmtfval 18908  cvrfval 18967  csubspset 19241  lineset 19497  psubspset 19503  psubclset 19696  lautset 19841  pautset 19862  tendoset 20584
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-sep 3609
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-ex 1521  df-sb 1765  df-clab 2080  df-cleq 2085  df-clel 2088  df-v 2501  df-in 2808  df-ss 2810
Copyright terms: Public domain