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

Theorem ssexi 4458
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 4457 . 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 1756   _Vcvv 2993    C_ wss 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363
This theorem is referenced by:  zfausab  4462  ord3ex  4503  epse  4724  opabex  5967  fvclex  6570  oprabex  6586  tfrlem16  6873  oev  6975  sbthlem2  7443  phplem2  7512  php  7516  pssnn  7552  dffi3  7702  inf3lem3  7857  r0weon  8200  dfac3  8312  dfac5lem4  8317  dfac2  8321  hsmexlem6  8621  domtriomlem  8632  axdc3lem  8640  ac6  8670  brdom7disj  8719  brdom6disj  8720  konigthlem  8753  niex  9071  enqex  9112  npex  9176  enrex  9258  axcnex  9335  reex  9394  nnex  10349  zex  10676  qex  10986  ixxex  11332  ltweuz  11805  1arithlem1  14005  1arith  14009  prdsval  14414  prdsle  14421  sectfval  14711  sscpwex  14749  issubc  14769  isfunc  14795  fullfunc  14837  fthfunc  14838  isfull  14841  isfth  14845  ipoval  15345  letsr  15418  nmznsg  15746  eqgfval  15750  isghm  15768  symgval  15905  ablfac1b  16593  lpival  17349  ltbval  17575  opsrle  17579  xrsle  17858  xrs10  17874  xrge0cmn  17877  znle  17989  cnmsgngrp  18031  psgninv  18034  cssval  18129  pjfval  18153  istopon  18552  leordtval2  18838  lecldbas  18845  xkoopn  19184  xkouni  19194  xkoccn  19214  xkoco1cn  19252  xkoco2cn  19253  xkococn  19255  xkoinjcn  19282  uzrest  19492  ustfn  19798  ustn0  19817  imasdsf1olem  19970  qtopbaslem  20359  isphtpc  20588  tchex  20754  tchnmfval  20765  bcthlem1  20857  bcthlem5  20861  dyadmbl  21102  itg2seq  21242  lhop1lem  21507  aannenlem3  21818  psercn  21913  abelth  21928  cxpcn2  22206  vmaval  22473  sqff1o  22542  musum  22553  vmadivsum  22753  rpvmasumlem  22758  mudivsum  22801  selberglem1  22816  selberglem2  22817  selberg2lem  22821  selberg2  22822  pntrsumo1  22836  selbergr  22839  iscgrg  22987  issubgoi  23819  sspval  24143  ajfval  24231  shex  24636  chex  24651  hmopex  25301  fpwrelmap  26055  ressplusf  26133  ressmulgnn  26166  inftmrel  26219  isinftm  26220  dmvlsiga  26594  measbase  26633  ismeas  26635  isrnmeas  26636  faeval  26684  eulerpartlemmf  26780  eulerpartlemgvv  26781  coinflippv  26888  ballotlemoex  26890  signsplypnf  26973  signsply0  26974  afsval  27017  kur14lem7  27122  kur14lem9  27124  dfon2lem7  27624  colinearex  28113  heibor1lem  28734  rrnval  28752  eldiophb  29121  pellexlem3  29198  pellexlem5  29200  setindtr  29399  onfrALTlem3VD  31719  lsatset  32731  lcvfbr  32761  cmtfvalN  32951  cvrfval  33009  lineset  33478  psubspset  33484  psubclsetN  33676  lautset  33822  pautsetN  33838  tendoset  34499  dicval  34917
  Copyright terms: Public domain W3C validator