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

Theorem ssel2 3631
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 3630 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
21imp 444 1 ((𝐴𝐵𝐶𝐴) → 𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  tz7.7  5787  onfr  5801  onmindif  5853  ordunisssuc  5868  ssimaex  6302  nssdmovg  6858  onnmin  7045  onmindif2  7054  limsssuc  7092  1st2nd  7258  f1o2ndf1  7330  dfrecs3  7514  boxriin  7992  ordunifi  8251  isfinite2  8259  ordtypelem7  8470  sucprcreg  8544  cnfcom  8635  coflim  9121  cflim2  9123  fin23lem11  9177  fin23lem26  9185  fin1a2lem13  9272  fpwwe2lem12  9501  suplem2pr  9913  axpre-sup  10028  axsup  10151  dedekind  10238  dedekindle  10239  lbinf  11014  dfinfre  11042  infrelb  11046  suprfinzcl  11530  uzwo  11789  supminf  11813  lbzbi  11814  zsupss  11815  suprzcl2  11816  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  supxr2  12182  supxrun  12184  supxrunb1  12187  supxrbnd1  12189  supxrbnd2  12190  supxrub  12192  supxrbnd  12196  infxrlb  12202  elfzom1elp1fzo  12574  ssfzo12  12601  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  fsuppmapnn0fiub0  12833  seqsplit  12874  shftlem  13852  rpnnen2lem10  14996  rpnnen2lem11  14997  gcdcllem1  15268  mrcuni  16328  isacs1i  16365  mreacs  16366  lubss  17168  gsumwspan  17430  subgint  17665  cntziinsn  17813  cntzsubg  17815  pmtrdifellem4  17945  subrgint  18850  cntzsubr  18860  mdetunilem9  20474  tgcl  20821  fctop  20856  cctop  20858  neips  20965  cmpsub  21251  1stcelcls  21312  ssref  21363  comppfsc  21383  txbasval  21457  fgss2  21725  filconn  21734  filuni  21736  filssufilg  21762  fmfnfmlem4  21808  trust  22080  elmopn2  22297  metrest  22376  dscopn  22425  metds0  22700  cncfmet  22758  negcncf  22768  iscmet2  23138  ovolfioo  23282  ovolficc  23283  itg1mulc  23516  ply1term  24005  plyconst  24007  reeff1olem  24245  usgruspgrb  26121  ocsh  28270  ocorth  28278  spansncvi  28639  pjss1coi  29150  sumdmdii  29402  dfcnv2  29604  xrge0infss  29653  measres  30413  measdivcstOLD  30415  measdivcst  30416  dya2iocuni  30473  bnj1190  31202  elintfv  31788  frrlem5e  31913  nosupno  31974  nosupbday  31976  nosupbnd1lem5  31983  noetalem3  31990  opnrebl  32440  opnrebl2  32441  fness  32469  fin2so  33526  matunitlindflem1  33535  poimirlem27  33566  poimir  33572  frinfm  33660  filbcmb  33665  nnubfi  33676  nninfnub  33677  sstotbnd3  33705  bndss  33715  exidreslem  33806  isidlc  33944  idlnegcl  33951  intidl  33958  unichnidl  33960  pmapglb2N  35375  elpaddn0  35404  paddasslem9  35432  paddasslem10  35433  pclfinN  35504  polval2N  35510  diaglbN  36661  dihord6apre  36862  gneispace  38749  snsslVD  39378  snssl  39379  sstrALT2VD  39383  sstrALT2  39384  suctrALTcf  39472  suctrALTcfVD  39473  ssnel  39518  uzwo4  39535  infxrunb2  39897  infxrbnd2  39898  supxrunb3  39936  unb2ltle  39955  infxrpnf  39987  supminfxr  40007  sge0iunmptlemfi  40948  caratheodorylem2  41062  ovnlerp  41097  ssfz12  41649  prssspr  42060  prsssprel  42063  lindslinindimp2lem4  42575  lindslinindsimp2  42577  lincresunit3lem2  42594  lincresunit3  42595
  Copyright terms: Public domain W3C validator