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

Theorem ssexi 4564
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 4563 . 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 1898   _Vcvv 3057    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430
This theorem is referenced by:  zfausab  4569  ord3ex  4610  epse  4839  opabex  6164  fvclex  6797  oprabex  6813  tfrlem16  7142  oev  7247  sbthlem2  7714  phplem2  7783  php  7787  pssnn  7821  dffi3  7976  inf3lem3  8166  r0weon  8474  dfac3  8583  dfac5lem4  8588  dfac2  8592  hsmexlem6  8892  domtriomlem  8903  axdc3lem  8911  ac6  8941  brdom7disj  8990  brdom6disj  8991  konigthlem  9024  niex  9337  enqex  9378  npex  9442  enrex  9522  axcnex  9602  reex  9661  nnex  10648  zex  10980  qex  11310  ixxex  11680  ltweuz  12213  prmex  14683  1arithlem1  14922  1arith  14926  prdsval  15408  prdsle  15415  sectfval  15711  sscpwex  15775  issubc  15795  isfunc  15824  fullfunc  15866  fthfunc  15867  isfull  15870  isfth  15874  ipoval  16455  letsr  16528  nmznsg  16916  eqgfval  16920  isghm  16938  symgval  17075  ablfac1b  17758  lpival  18524  ltbval  18750  opsrle  18754  xrsle  19043  xrs10  19062  xrge0cmn  19065  znle  19162  cnmsgngrp  19202  psgninv  19205  cssval  19300  pjfval  19324  istopon  19995  leordtval2  20283  lecldbas  20290  xkoopn  20659  xkouni  20669  xkoccn  20689  xkoco1cn  20727  xkoco2cn  20728  xkococn  20730  xkoinjcn  20757  uzrest  20967  ustfn  21271  ustn0  21290  imasdsf1olem  21443  qtopbaslem  21834  isphtpc  22080  tchex  22246  tchnmfval  22257  bcthlem1  22347  bcthlem5  22351  dyadmbl  22614  itg2seq  22756  lhop1lem  23021  aannenlem3  23342  psercn  23437  abelth  23452  cxpcn2  23742  vmaval  24096  sqff1o  24165  musum  24176  vmadivsum  24376  rpvmasumlem  24381  mudivsum  24424  selberglem1  24439  selberglem2  24440  selberg2lem  24444  selberg2  24445  pntrsumo1  24459  selbergr  24462  iscgrg  24613  isismt  24635  ishlg  24703  ishpg  24857  iscgra  24907  isinag  24935  isleag  24939  issubgoi  26094  sspval  26418  ajfval  26506  shex  26921  chex  26935  hmopex  27584  ressplusf  28463  ressmulgnn  28497  inftmrel  28548  isinftm  28549  dmvlsiga  29002  measbase  29070  ismeas  29072  isrnmeas  29073  faeval  29119  eulerpartlemmf  29258  eulerpartlemgvv  29259  signsplypnf  29489  signsply0  29490  afsval  29538  kur14lem7  29985  kur14lem9  29987  mppsval  30260  dfon2lem7  30485  colinearex  30877  poimirlem4  31990  heibor1lem  32187  rrnval  32205  lsatset  32602  lcvfbr  32632  cmtfvalN  32822  cvrfval  32880  lineset  33349  psubspset  33355  psubclsetN  33547  lautset  33693  pautsetN  33709  tendoset  34372  dicval  34790  eldiophb  35645  pellexlem3  35721  pellexlem5  35723  setindtr  35925  onfrALTlem3VD  37325  dmvolsal  38306  pthsfval  39851  spthsfval  39852  crctS  39907  cyclS  39908
  Copyright terms: Public domain W3C validator