MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssexi Unicode version

Theorem ssexi 4159
Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
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 4158 . 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 1684   _Vcvv 2788    C_ wss 3152
This theorem is referenced by:  zfausab  4163  ord3ex  4200  epse  4376  opabex  5744  fvclex  5761  oprabex  5961  tfrlem16  6409  oev  6513  sbthlem2  6972  phplem2  7041  php  7045  pssnn  7081  dffi3  7184  inf3lem3  7331  r0weon  7640  dfac3  7748  dfac5lem4  7753  dfac2  7757  hsmexlem6  8057  domtriomlem  8068  axdc3lem  8076  ac6  8107  brdom7disj  8156  brdom6disj  8157  konigthlem  8190  niex  8505  enqex  8546  npex  8610  enrex  8692  axcnex  8769  reex  8828  nnex  9752  zex  10033  qex  10328  ixxex  10667  ltweuz  11024  1arithlem1  12970  1arith  12974  prdsval  13355  prdsle  13361  sectfval  13654  sscpwex  13692  issubc  13712  isfunc  13738  fullfunc  13780  fthfunc  13781  isfull  13784  isfth  13788  ipoval  14257  letsr  14349  nmznsg  14661  eqgfval  14665  isghm  14683  symgval  14771  ablfac1b  15305  lpival  15997  ltbval  16213  opsrle  16217  xrsle  16394  xrs10  16410  xrge0cmn  16413  znle  16490  cssval  16582  pjfval  16606  istopon  16663  leordtval2  16942  lecldbas  16949  xkoopn  17284  xkouni  17294  xkoccn  17313  xkoco1cn  17351  xkoco2cn  17352  xkococn  17354  xkoinjcn  17381  uzrest  17592  imasdsf1olem  17937  qtopbaslem  18267  isphtpc  18492  tchex  18649  tchnmfval  18659  bcthlem1  18746  bcthlem5  18750  dyadmbl  18955  itg2seq  19097  lhop1lem  19360  aannenlem3  19710  psercn  19802  abelth  19817  cxpcn2  20086  vmaval  20351  vmaf  20357  sqff1o  20420  musum  20431  vmadivsum  20631  rpvmasumlem  20636  mudivsum  20679  selberglem1  20694  selberglem2  20695  selberg2lem  20699  selberg2  20700  pntrsumo1  20714  selbergr  20717  issubgoi  20977  sspval  21299  ajfval  21387  shex  21791  chex  21806  hmopex  22455  ballotlemoex  23044  ressplusf  23298  ressmulgnn  23308  dmvlsiga  23490  sigagensiga  23502  isrnmeas  23531  coinflippv  23684  kur14lem7  23743  kur14lem9  23745  dfon2lem7  24145  colinearex  24683  prodex  25304  isrocatset  25957  heibor1lem  26533  rrnval  26551  eldiophb  26836  pellexlem3  26916  pellexlem5  26918  setindtr  27117  cnmsgngrp  27436  onfrALTlem3VD  28663  lsatset  29180  lcvfbr  29210  cmtfvalN  29400  cvrfval  29458  lineset  29927  psubspset  29933  psubclsetN  30125  lautset  30271  pautsetN  30287  tendoset  30948  dicval  31366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator