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

Theorem ssexi 4175
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 4174 . 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 1696   _Vcvv 2801    C_ wss 3165
This theorem is referenced by:  zfausab  4179  ord3ex  4216  epse  4392  opabex  5760  fvclex  5777  oprabex  5977  tfrlem16  6425  oev  6529  sbthlem2  6988  phplem2  7057  php  7061  pssnn  7097  dffi3  7200  inf3lem3  7347  r0weon  7656  dfac3  7764  dfac5lem4  7769  dfac2  7773  hsmexlem6  8073  domtriomlem  8084  axdc3lem  8092  ac6  8123  brdom7disj  8172  brdom6disj  8173  konigthlem  8206  niex  8521  enqex  8562  npex  8626  enrex  8708  axcnex  8785  reex  8844  nnex  9768  zex  10049  qex  10344  ixxex  10683  ltweuz  11040  1arithlem1  12986  1arith  12990  prdsval  13371  prdsle  13377  sectfval  13670  sscpwex  13708  issubc  13728  isfunc  13754  fullfunc  13796  fthfunc  13797  isfull  13800  isfth  13804  ipoval  14273  letsr  14365  nmznsg  14677  eqgfval  14681  isghm  14699  symgval  14787  ablfac1b  15321  lpival  16013  ltbval  16229  opsrle  16233  xrsle  16410  xrs10  16426  xrge0cmn  16429  znle  16506  cssval  16598  pjfval  16622  istopon  16679  leordtval2  16958  lecldbas  16965  xkoopn  17300  xkouni  17310  xkoccn  17329  xkoco1cn  17367  xkoco2cn  17368  xkococn  17370  xkoinjcn  17397  uzrest  17608  imasdsf1olem  17953  qtopbaslem  18283  isphtpc  18508  tchex  18665  tchnmfval  18675  bcthlem1  18762  bcthlem5  18766  dyadmbl  18971  itg2seq  19113  lhop1lem  19376  aannenlem3  19726  psercn  19818  abelth  19833  cxpcn2  20102  vmaval  20367  vmaf  20373  sqff1o  20436  musum  20447  vmadivsum  20647  rpvmasumlem  20652  mudivsum  20695  selberglem1  20710  selberglem2  20711  selberg2lem  20715  selberg2  20716  pntrsumo1  20730  selbergr  20733  issubgoi  20993  sspval  21315  ajfval  21403  shex  21807  chex  21822  hmopex  22471  ballotlemoex  23060  ressplusf  23313  ressmulgnn  23323  dmvlsiga  23505  sigagensiga  23517  isrnmeas  23546  coinflippv  23699  kur14lem7  23758  kur14lem9  23760  dfon2lem7  24216  colinearex  24755  prodex  25407  isrocatset  26060  heibor1lem  26636  rrnval  26654  eldiophb  26939  pellexlem3  27019  pellexlem5  27021  setindtr  27220  cnmsgngrp  27539  onfrALTlem3VD  28979  lsatset  29802  lcvfbr  29832  cmtfvalN  30022  cvrfval  30080  lineset  30549  psubspset  30555  psubclsetN  30747  lautset  30893  pautsetN  30909  tendoset  31570  dicval  31988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator