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

Theorem ssexi 4099
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 4098 . 2  |-  ( A 
C_  B  ->  A  e.  _V )
41, 3ax-mp 10 1  |-  A  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2740    C_ wss 3094
This theorem is referenced by:  zfausab  4103  ord3ex  4138  epse  4313  opabex  5643  fvclex  5660  oprabex  5860  tfrlem16  6342  oev  6446  sbthlem2  6905  phplem2  6974  php  6978  pssnn  7014  dffi3  7117  inf3lem3  7264  r0weon  7573  dfac3  7681  dfac5lem4  7686  dfac2  7690  hsmexlem6  7990  domtriomlem  8001  axdc3lem  8009  ac6  8040  brdom7disj  8089  brdom6disj  8090  konigthlem  8123  niex  8438  enqex  8479  npex  8543  enrex  8625  axcnex  8702  reex  8761  nnex  9685  zex  9965  qex  10260  ixxex  10598  ltweuz  10955  1arithlem1  12897  1arith  12901  prdsval  13282  prdsle  13288  sectfval  13581  sscpwex  13619  issubc  13639  isfunc  13665  fullfunc  13707  fthfunc  13708  isfull  13711  isfth  13715  ipoval  14184  letsr  14276  nmznsg  14588  eqgfval  14592  isghm  14610  symgval  14698  ablfac1b  15232  lpival  15924  ltbval  16140  opsrle  16144  xrsle  16321  xrs10  16337  xrge0cmn  16340  znle  16417  cssval  16509  pjfval  16533  istopon  16590  leordtval2  16869  lecldbas  16876  xkoopn  17211  xkouni  17221  xkoccn  17240  xkoco1cn  17278  xkoco2cn  17279  xkococn  17281  xkoinjcn  17308  uzrest  17519  imasdsf1olem  17864  qtopbaslem  18194  isphtpc  18419  tchex  18576  tchnmfval  18586  bcthlem1  18673  bcthlem5  18677  dyadmbl  18882  itg2seq  19024  lhop1lem  19287  aannenlem3  19637  psercn  19729  abelth  19744  cxpcn2  20013  vmaval  20278  vmaf  20284  sqff1o  20347  musum  20358  vmadivsum  20558  rpvmasumlem  20563  mudivsum  20606  selberglem1  20621  selberglem2  20622  selberg2lem  20626  selberg2  20627  pntrsumo1  20641  selbergr  20644  issubgoi  20902  sspval  21224  ajfval  21312  shex  21716  chex  21731  hmopex  22380  ballotlemoex  22970  kur14lem7  23080  kur14lem9  23082  dfon2lem7  23479  colinearex  24023  prodex  24636  isrocatset  25289  heibor1lem  25865  rrnval  25883  eldiophb  26168  pellexlem3  26248  pellexlem5  26250  setindtr  26449  cnmsgngrp  26768  onfrALTlem3VD  27676  lsatset  28310  lcvfbr  28340  cmtfvalN  28530  cvrfval  28588  lineset  29057  psubspset  29063  psubclsetN  29255  lautset  29401  pautsetN  29417  tendoset  30078  dicval  30496
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator