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

Theorem ssexi 4582
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 4581 . 2  |-  ( A 
C_  B  ->  A  e.  _V )
41, 3ax-mp 5 1  |-  A  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   _Vcvv 3095    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475
This theorem is referenced by:  zfausab  4586  ord3ex  4627  epse  4852  opabex  6126  fvclex  6757  oprabex  6773  tfrlem16  7064  oev  7166  sbthlem2  7630  phplem2  7699  php  7703  pssnn  7740  dffi3  7893  inf3lem3  8050  r0weon  8393  dfac3  8505  dfac5lem4  8510  dfac2  8514  hsmexlem6  8814  domtriomlem  8825  axdc3lem  8833  ac6  8863  brdom7disj  8912  brdom6disj  8913  konigthlem  8946  niex  9262  enqex  9303  npex  9367  enrex  9447  axcnex  9527  reex  9586  nnex  10549  zex  10880  qex  11205  ixxex  11551  ltweuz  12054  1arithlem1  14423  1arith  14427  prdsval  14834  prdsle  14841  sectfval  15128  sscpwex  15166  issubc  15186  isfunc  15212  fullfunc  15254  fthfunc  15255  isfull  15258  isfth  15262  ipoval  15763  letsr  15836  nmznsg  16224  eqgfval  16228  isghm  16246  symgval  16383  ablfac1b  17100  lpival  17872  ltbval  18115  opsrle  18119  xrsle  18417  xrs10  18436  xrge0cmn  18439  znle  18551  cnmsgngrp  18593  psgninv  18596  cssval  18691  pjfval  18715  istopon  19404  leordtval2  19691  lecldbas  19698  xkoopn  20068  xkouni  20078  xkoccn  20098  xkoco1cn  20136  xkoco2cn  20137  xkococn  20139  xkoinjcn  20166  uzrest  20376  ustfn  20682  ustn0  20701  imasdsf1olem  20854  qtopbaslem  21243  isphtpc  21472  tchex  21638  tchnmfval  21649  bcthlem1  21741  bcthlem5  21745  dyadmbl  21987  itg2seq  22127  lhop1lem  22392  aannenlem3  22704  psercn  22799  abelth  22814  cxpcn2  23098  vmaval  23365  sqff1o  23434  musum  23445  vmadivsum  23645  rpvmasumlem  23650  mudivsum  23693  selberglem1  23708  selberglem2  23709  selberg2lem  23713  selberg2  23714  pntrsumo1  23728  selbergr  23731  iscgrg  23882  isismt  23899  ishlg  23964  ishpg  24106  iscgra  24147  issubgoi  25290  sspval  25614  ajfval  25702  shex  26107  chex  26122  hmopex  26772  ressplusf  27616  ressmulgnn  27649  inftmrel  27702  isinftm  27703  dmvlsiga  28107  measbase  28146  ismeas  28148  isrnmeas  28149  faeval  28196  eulerpartlemmf  28292  eulerpartlemgvv  28293  signsplypnf  28485  signsply0  28486  afsval  28529  kur14lem7  28634  kur14lem9  28636  mppsval  28910  dfon2lem7  29197  colinearex  29686  heibor1lem  30281  rrnval  30299  eldiophb  30666  pellexlem3  30743  pellexlem5  30745  setindtr  30942  etransclem25  31996  etransclem35  32006  onfrALTlem3VD  33555  lsatset  34590  lcvfbr  34620  cmtfvalN  34810  cvrfval  34868  lineset  35337  psubspset  35343  psubclsetN  35535  lautset  35681  pautsetN  35697  tendoset  36360  dicval  36778
  Copyright terms: Public domain W3C validator