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

Theorem ssexi 4592
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 4591 . 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 1767   _Vcvv 3113    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490
This theorem is referenced by:  zfausab  4596  ord3ex  4637  epse  4862  opabex  6129  fvclex  6756  oprabex  6772  tfrlem16  7062  oev  7164  sbthlem2  7628  phplem2  7697  php  7701  pssnn  7738  dffi3  7891  inf3lem3  8047  r0weon  8390  dfac3  8502  dfac5lem4  8507  dfac2  8511  hsmexlem6  8811  domtriomlem  8822  axdc3lem  8830  ac6  8860  brdom7disj  8909  brdom6disj  8910  konigthlem  8943  niex  9259  enqex  9300  npex  9364  enrex  9444  axcnex  9524  reex  9583  nnex  10542  zex  10873  qex  11194  ixxex  11540  ltweuz  12040  1arithlem1  14300  1arith  14304  prdsval  14710  prdsle  14717  sectfval  15007  sscpwex  15045  issubc  15065  isfunc  15091  fullfunc  15133  fthfunc  15134  isfull  15137  isfth  15141  ipoval  15641  letsr  15714  nmznsg  16050  eqgfval  16054  isghm  16072  symgval  16209  ablfac1b  16923  lpival  17692  ltbval  17935  opsrle  17939  xrsle  18237  xrs10  18253  xrge0cmn  18256  znle  18368  cnmsgngrp  18410  psgninv  18413  cssval  18508  pjfval  18532  istopon  19221  leordtval2  19507  lecldbas  19514  xkoopn  19853  xkouni  19863  xkoccn  19883  xkoco1cn  19921  xkoco2cn  19922  xkococn  19924  xkoinjcn  19951  uzrest  20161  ustfn  20467  ustn0  20486  imasdsf1olem  20639  qtopbaslem  21028  isphtpc  21257  tchex  21423  tchnmfval  21434  bcthlem1  21526  bcthlem5  21530  dyadmbl  21772  itg2seq  21912  lhop1lem  22177  aannenlem3  22488  psercn  22583  abelth  22598  cxpcn2  22876  vmaval  23143  sqff1o  23212  musum  23223  vmadivsum  23423  rpvmasumlem  23428  mudivsum  23471  selberglem1  23486  selberglem2  23487  selberg2lem  23491  selberg2  23492  pntrsumo1  23506  selbergr  23509  iscgrg  23660  isismt  23677  issubgoi  25016  sspval  25340  ajfval  25428  shex  25833  chex  25848  hmopex  26498  fpwrelmap  27256  ressplusf  27328  ressmulgnn  27361  inftmrel  27414  isinftm  27415  dmvlsiga  27797  measbase  27836  ismeas  27838  isrnmeas  27839  faeval  27886  eulerpartlemmf  27982  eulerpartlemgvv  27983  coinflippv  28090  ballotlemoex  28092  signsplypnf  28175  signsply0  28176  afsval  28219  kur14lem7  28324  kur14lem9  28326  dfon2lem7  28826  colinearex  29315  heibor1lem  29936  rrnval  29954  eldiophb  30322  pellexlem3  30399  pellexlem5  30401  setindtr  30598  onfrALTlem3VD  32785  lsatset  33805  lcvfbr  33835  cmtfvalN  34025  cvrfval  34083  lineset  34552  psubspset  34558  psubclsetN  34750  lautset  34896  pautsetN  34912  tendoset  35573  dicval  35991
  Copyright terms: Public domain W3C validator