Theorem ssel2 3978

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)

Assertion

Ref	Expression
ssel2	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Proof of Theorem ssel2

Step	Hyp	Ref	Expression
1		ssel 3976	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
2	1	imp 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  tz7.7  6391  onfr  6404  onmindif  6457  ordunisssuc  6471  ssimaex  6977  nssdmovg  7589  onnmin  7786  onmindif2  7795  limsssuc  7839  el2xpss  8023  1st2nd  8025  f1o2ndf1  8108  dfrecs3  8372  dfrecs3OLD  8373  boxriin  8934  ordunifi  9293  isfinite2  9301  ordtypelem7  9519  sucprcreg  9596  cnfcom  9695  eldju1st  9918  coflim  10256  cflim2  10258  fin23lem11  10312  fin23lem26  10320  fin1a2lem13  10407  fpwwe2lem11  10636  suplem2pr  11048  axpre-sup  11164  axsup  11289  dedekind  11377  dedekindle  11378  fimaxre  12158  fiminre  12161  lbinf  12167  dfinfre  12195  infrelb  12199  suprfinzcl  12676  uzwo  12895  supminf  12919  lbzbi  12920  zsupss  12921  suprzcl2  12922  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  supxr2  13293  supxrun  13295  supxrunb1  13298  supxrbnd1  13300  supxrbnd2  13301  supxrub  13303  supxrbnd  13307  infxrlb  13313  elfzom1elp1fzo  13699  ssfzo12  13725  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiub0  13958  seqsplit  14001  shftlem  15015  rpnnen2lem10  16166  rpnnen2lem11  16167  gcdcllem1  16440  mrcuni  17565  isacs1i  17601  mreacs  17602  lubss  18466  gsumwspan  18727  subgint  19030  cntziinsn  19201  cntzsubg  19203  pmtrdifellem4  19347  subrgint  20342  cntzsubr  20353  sraassab  21422  mdetunilem9  22122  tgcl  22472  fctop  22507  cctop  22509  neips  22617  cmpsub  22904  1stcelcls  22965  ssref  23016  comppfsc  23036  txbasval  23110  fgss2  23378  filconn  23387  filuni  23389  filssufilg  23415  fmfnfmlem4  23461  trust  23734  elmopn2  23951  metrest  24033  dscopn  24082  metds0  24366  cncfmet  24425  negcncf  24438  iscmet2  24811  ovolfioo  24984  ovolficc  24985  itg1mulc  25222  ply1term  25718  plyconst  25720  reeff1olem  25958  nosupno  27206  nosupbday  27208  nosupbnd1lem5  27215  noinfno  27221  noinfbday  27223  noetasuplem4  27239  usgruspgrb  28441  ocsh  30536  ocorth  30544  spansncvi  30905  pjss1coi  31416  sumdmdii  31668  unidifsnel  31772  dfcnv2  31901  xrge0infss  31973  measdivcst  33222  measdivcstALTV  33223  dya2iocuni  33282  bnj1190  34019  nummin  34094  gg-negcncf  35166  opnrebl  35205  opnrebl2  35206  fness  35234  nlpineqsn  36289  fin2so  36475  matunitlindflem1  36484  poimirlem27  36515  poimir  36521  frinfm  36603  filbcmb  36608  nnubfi  36618  nninfnub  36619  sstotbnd3  36644  bndss  36654  exidreslem  36745  isidlc  36883  idlnegcl  36890  intidl  36897  unichnidl  36899  pmapglb2N  38642  elpaddn0  38671  paddasslem9  38699  paddasslem10  38700  pclfinN  38771  polval2N  38777  diaglbN  39926  dihord6apre  40127  unielss  41967  onmaxnelsup  41972  onsupmaxb  41988  onsupeqnmax  41996  gneispace  42885  snsslVD  43590  snssl  43591  sstrALT2VD  43595  sstrALT2  43596  suctrALTcf  43683  suctrALTcfVD  43684  ssnel  43727  uzwo4  43740  infxrunb2  44078  infxrbnd2  44079  supxrunb3  44109  unb2ltle  44125  infxrpnf  44156  supminfxr  44174  sge0iunmptlemfi  45129  caratheodorylem2  45243  ovnlerp  45278  ssfz12  46022  prssspr  46153  prsssprel  46156  subrngint  46739  cntzsubrng  46746  lindslinindimp2lem4  47142  lindslinindsimp2  47144  lincresunit3lem2  47161  lincresunit3  47162