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

Theorem ssexi 4425
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 4424 . 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 1755   _Vcvv 2962    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330
This theorem is referenced by:  zfausab  4429  ord3ex  4470  epse  4690  opabex  5933  fvclex  6538  oprabex  6554  tfrlem16  6838  oev  6942  sbthlem2  7410  phplem2  7479  php  7483  pssnn  7519  dffi3  7669  inf3lem3  7824  r0weon  8167  dfac3  8279  dfac5lem4  8284  dfac2  8288  hsmexlem6  8588  domtriomlem  8599  axdc3lem  8607  ac6  8637  brdom7disj  8686  brdom6disj  8687  konigthlem  8720  niex  9037  enqex  9078  npex  9142  enrex  9224  axcnex  9301  reex  9360  nnex  10315  zex  10642  qex  10952  ixxex  11298  ltweuz  11767  1arithlem1  13966  1arith  13970  prdsval  14375  prdsle  14382  sectfval  14672  sscpwex  14710  issubc  14730  isfunc  14756  fullfunc  14798  fthfunc  14799  isfull  14802  isfth  14806  ipoval  15306  letsr  15379  nmznsg  15704  eqgfval  15708  isghm  15726  symgval  15863  ablfac1b  16544  lpival  17248  ltbval  17484  opsrle  17488  xrsle  17679  xrs10  17695  xrge0cmn  17698  znle  17808  cnmsgngrp  17850  psgninv  17853  cssval  17948  pjfval  17972  istopon  18371  leordtval2  18657  lecldbas  18664  xkoopn  19003  xkouni  19013  xkoccn  19033  xkoco1cn  19071  xkoco2cn  19072  xkococn  19074  xkoinjcn  19101  uzrest  19311  ustfn  19617  ustn0  19636  imasdsf1olem  19789  qtopbaslem  20178  isphtpc  20407  tchex  20573  tchnmfval  20584  bcthlem1  20676  bcthlem5  20680  dyadmbl  20921  itg2seq  21061  lhop1lem  21326  aannenlem3  21680  psercn  21775  abelth  21790  cxpcn2  22068  vmaval  22335  sqff1o  22404  musum  22415  vmadivsum  22615  rpvmasumlem  22620  mudivsum  22663  selberglem1  22678  selberglem2  22679  selberg2lem  22683  selberg2  22684  pntrsumo1  22698  selbergr  22701  iscgrg  22845  issubgoi  23619  sspval  23943  ajfval  24031  shex  24436  chex  24451  hmopex  25101  fpwrelmap  25857  ressplusf  25933  ressmulgnn  25966  inftmrel  26020  isinftm  26021  dmvlsiga  26425  measbase  26464  ismeas  26466  isrnmeas  26467  faeval  26515  eulerpartlem1  26597  eulerpartlemmf  26605  eulerpartlemgvv  26606  coinflippv  26713  ballotlemoex  26715  signsplypnf  26798  signsply0  26799  afsval  26842  kur14lem7  26947  kur14lem9  26949  dfon2lem7  27448  colinearex  27937  heibor1lem  28549  rrnval  28567  eldiophb  28937  pellexlem3  29014  pellexlem5  29016  setindtr  29215  onfrALTlem3VD  31322  lsatset  32205  lcvfbr  32235  cmtfvalN  32425  cvrfval  32483  lineset  32952  psubspset  32958  psubclsetN  33150  lautset  33296  pautsetN  33312  tendoset  33973  dicval  34391
  Copyright terms: Public domain W3C validator