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

Theorem ssexi 4510
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 4509 . 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 1826   _Vcvv 3034    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396  df-ss 3403
This theorem is referenced by:  zfausab  4514  ord3ex  4555  epse  4776  opabex  6042  fvclex  6671  oprabex  6687  tfrlem16  6980  oev  7082  sbthlem2  7547  phplem2  7616  php  7620  pssnn  7654  dffi3  7806  inf3lem3  7961  r0weon  8303  dfac3  8415  dfac5lem4  8420  dfac2  8424  hsmexlem6  8724  domtriomlem  8735  axdc3lem  8743  ac6  8773  brdom7disj  8822  brdom6disj  8823  konigthlem  8856  niex  9170  enqex  9211  npex  9275  enrex  9355  axcnex  9435  reex  9494  nnex  10458  zex  10790  qex  11113  ixxex  11461  ltweuz  11975  1arithlem1  14443  1arith  14447  prdsval  14862  prdsle  14869  sectfval  15157  sscpwex  15221  issubc  15241  isfunc  15270  fullfunc  15312  fthfunc  15313  isfull  15316  isfth  15320  ipoval  15901  letsr  15974  nmznsg  16362  eqgfval  16366  isghm  16384  symgval  16521  ablfac1b  17234  lpival  18006  ltbval  18249  opsrle  18253  xrsle  18551  xrs10  18570  xrge0cmn  18573  znle  18666  cnmsgngrp  18706  psgninv  18709  cssval  18804  pjfval  18828  istopon  19511  leordtval2  19799  lecldbas  19806  xkoopn  20175  xkouni  20185  xkoccn  20205  xkoco1cn  20243  xkoco2cn  20244  xkococn  20246  xkoinjcn  20273  uzrest  20483  ustfn  20789  ustn0  20808  imasdsf1olem  20961  qtopbaslem  21350  isphtpc  21579  tchex  21745  tchnmfval  21756  bcthlem1  21848  bcthlem5  21852  dyadmbl  22094  itg2seq  22234  lhop1lem  22499  aannenlem3  22811  psercn  22906  abelth  22921  cxpcn2  23207  vmaval  23504  sqff1o  23573  musum  23584  vmadivsum  23784  rpvmasumlem  23789  mudivsum  23832  selberglem1  23847  selberglem2  23848  selberg2lem  23852  selberg2  23853  pntrsumo1  23867  selbergr  23870  iscgrg  24024  isismt  24041  ishlg  24106  ishpg  24248  iscgra  24289  issubgoi  25429  sspval  25753  ajfval  25841  shex  26246  chex  26261  hmopex  26910  ressplusf  27791  ressmulgnn  27824  inftmrel  27877  isinftm  27878  dmvlsiga  28278  measbase  28324  ismeas  28326  isrnmeas  28327  faeval  28374  eulerpartlemmf  28497  eulerpartlemgvv  28498  signsplypnf  28690  signsply0  28691  afsval  28734  kur14lem7  28845  kur14lem9  28847  mppsval  29121  dfon2lem7  29386  colinearex  29863  heibor1lem  30471  rrnval  30489  eldiophb  30855  pellexlem3  30932  pellexlem5  30934  setindtr  31132  onfrALTlem3VD  34034  lsatset  35128  lcvfbr  35158  cmtfvalN  35348  cvrfval  35406  lineset  35875  psubspset  35881  psubclsetN  36073  lautset  36219  pautsetN  36235  tendoset  36898  dicval  37316
  Copyright terms: Public domain W3C validator