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

Theorem ssexi 4160
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 4159 . 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 1685   _Vcvv 2789    C_ wss 3153
This theorem is referenced by:  zfausab  4164  ord3ex  4199  epse  4375  opabex  5706  fvclex  5723  oprabex  5923  tfrlem16  6405  oev  6509  sbthlem2  6968  phplem2  7037  php  7041  pssnn  7077  dffi3  7180  inf3lem3  7327  r0weon  7636  dfac3  7744  dfac5lem4  7749  dfac2  7753  hsmexlem6  8053  domtriomlem  8064  axdc3lem  8072  ac6  8103  brdom7disj  8152  brdom6disj  8153  konigthlem  8186  niex  8501  enqex  8542  npex  8606  enrex  8688  axcnex  8765  reex  8824  nnex  9748  zex  10029  qex  10324  ixxex  10663  ltweuz  11020  1arithlem1  12966  1arith  12970  prdsval  13351  prdsle  13357  sectfval  13650  sscpwex  13688  issubc  13708  isfunc  13734  fullfunc  13776  fthfunc  13777  isfull  13780  isfth  13784  ipoval  14253  letsr  14345  nmznsg  14657  eqgfval  14661  isghm  14679  symgval  14767  ablfac1b  15301  lpival  15993  ltbval  16209  opsrle  16213  xrsle  16390  xrs10  16406  xrge0cmn  16409  znle  16486  cssval  16578  pjfval  16602  istopon  16659  leordtval2  16938  lecldbas  16945  xkoopn  17280  xkouni  17290  xkoccn  17309  xkoco1cn  17347  xkoco2cn  17348  xkococn  17350  xkoinjcn  17377  uzrest  17588  imasdsf1olem  17933  qtopbaslem  18263  isphtpc  18488  tchex  18645  tchnmfval  18655  bcthlem1  18742  bcthlem5  18746  dyadmbl  18951  itg2seq  19093  lhop1lem  19356  aannenlem3  19706  psercn  19798  abelth  19813  cxpcn2  20082  vmaval  20347  vmaf  20353  sqff1o  20416  musum  20427  vmadivsum  20627  rpvmasumlem  20632  mudivsum  20675  selberglem1  20690  selberglem2  20691  selberg2lem  20695  selberg2  20696  pntrsumo1  20710  selbergr  20713  issubgoi  20971  sspval  21293  ajfval  21381  shex  21787  chex  21802  hmopex  22451  ballotlemoex  23040  kur14lem7  23150  kur14lem9  23152  dfon2lem7  23549  colinearex  24093  prodex  24715  isrocatset  25368  heibor1lem  25944  rrnval  25962  eldiophb  26247  pellexlem3  26327  pellexlem5  26329  setindtr  26528  cnmsgngrp  26847  onfrALTlem3VD  27943  lsatset  28459  lcvfbr  28489  cmtfvalN  28679  cvrfval  28737  lineset  29206  psubspset  29212  psubclsetN  29404  lautset  29550  pautsetN  29566  tendoset  30227  dicval  30645
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator