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

Theorem ssel2 3961
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
Assertion
Ref Expression
ssel2 ((𝐴𝐵𝐶𝐴) → 𝐶𝐵)

Proof of Theorem ssel2
StepHypRef Expression
1 ssel 3960 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
21imp 407 1 ((𝐴𝐵𝐶𝐴) → 𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  tz7.7  6211  onfr  6224  onmindif  6274  ordunisssuc  6287  ssimaex  6742  nssdmovg  7319  onnmin  7506  onmindif2  7515  limsssuc  7553  1st2nd  7729  f1o2ndf1  7809  dfrecs3  8000  boxriin  8493  ordunifi  8757  isfinite2  8765  ordtypelem7  8977  sucprcreg  9054  cnfcom  9152  eldju1st  9341  coflim  9672  cflim2  9674  fin23lem11  9728  fin23lem26  9736  fin1a2lem13  9823  fpwwe2lem12  10052  suplem2pr  10464  axpre-sup  10580  axsup  10705  dedekind  10792  dedekindle  10793  fimaxre  11573  fiminre  11577  lbinf  11583  dfinfre  11611  infrelb  11615  suprfinzcl  12086  uzwo  12300  supminf  12324  lbzbi  12325  zsupss  12326  suprzcl2  12327  xrsupsslem  12690  xrinfmsslem  12691  xrub  12695  supxr2  12697  supxrun  12699  supxrunb1  12702  supxrbnd1  12704  supxrbnd2  12705  supxrub  12707  supxrbnd  12711  infxrlb  12717  elfzom1elp1fzo  13094  ssfzo12  13120  fsuppmapnn0fiublem  13348  fsuppmapnn0fiub  13349  fsuppmapnn0fiub0  13351  seqsplit  13393  shftlem  14417  rpnnen2lem10  15566  rpnnen2lem11  15567  gcdcllem1  15838  mrcuni  16882  isacs1i  16918  mreacs  16919  lubss  17721  gsumwspan  18001  subgint  18243  cntziinsn  18405  cntzsubg  18407  pmtrdifellem4  18538  subrgint  19488  cntzsubr  19499  mdetunilem9  21159  tgcl  21507  fctop  21542  cctop  21544  neips  21651  cmpsub  21938  1stcelcls  21999  ssref  22050  comppfsc  22070  txbasval  22144  fgss2  22412  filconn  22421  filuni  22423  filssufilg  22449  fmfnfmlem4  22495  trust  22767  elmopn2  22984  metrest  23063  dscopn  23112  metds0  23387  cncfmet  23445  negcncf  23455  iscmet2  23826  ovolfioo  23997  ovolficc  23998  itg1mulc  24234  ply1term  24723  plyconst  24725  reeff1olem  24963  usgruspgrb  26894  ocsh  28988  ocorth  28996  spansncvi  29357  pjss1coi  29868  sumdmdii  30120  unidifsnel  30223  dfcnv2  30351  xrge0infss  30411  measres  31381  measdivcst  31383  measdivcstALTV  31384  dya2iocuni  31441  bnj1190  32178  nosupno  33101  nosupbday  33103  nosupbnd1lem5  33110  noetalem3  33117  opnrebl  33566  opnrebl2  33567  fness  33595  nlpineqsn  34572  fin2so  34761  matunitlindflem1  34770  poimirlem27  34801  poimir  34807  frinfm  34893  filbcmb  34898  nnubfi  34908  nninfnub  34909  sstotbnd3  34937  bndss  34947  exidreslem  35038  isidlc  35176  idlnegcl  35183  intidl  35190  unichnidl  35192  pmapglb2N  36789  elpaddn0  36818  paddasslem9  36846  paddasslem10  36847  pclfinN  36918  polval2N  36924  diaglbN  38073  dihord6apre  38274  gneispace  40364  snsslVD  41043  snssl  41044  sstrALT2VD  41048  sstrALT2  41049  suctrALTcf  41136  suctrALTcfVD  41137  ssnel  41182  uzwo4  41195  infxrunb2  41516  infxrbnd2  41517  supxrunb3  41552  unb2ltle  41569  infxrpnf  41601  supminfxr  41620  sge0iunmptlemfi  42576  caratheodorylem2  42690  ovnlerp  42725  ssfz12  43395  prssspr  43494  prsssprel  43497  lindslinindimp2lem4  44414  lindslinindsimp2  44416  lincresunit3lem2  44433  lincresunit3  44434
  Copyright terms: Public domain W3C validator