Theorem ssel2 3917

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 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
2	1	imp 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2815  df-ss 3907

This theorem is referenced by:  tz7.7  6343  onfr  6356  onmindif  6411  ordunisssuc  6425  ssimaex  6919  nssdmovg  7545  onnmin  7748  onmindif2  7757  limsssuc  7797  el2xpss  7986  1st2nd  7988  f1o2ndf1  8068  dfrecs3  8309  boxriin  8885  ordunifi  9197  isfinite2  9205  ordtypelem7  9436  sucprcregOLD  9519  cnfcom  9619  eldju1st  9845  coflim  10181  cflim2  10183  fin23lem11  10237  fin23lem26  10245  fin1a2lem13  10332  fpwwe2lem11  10562  suplem2pr  10974  axpre-sup  11090  axsup  11219  dedekind  11307  dedekindle  11308  fimaxre  12098  fiminre  12101  lbinf  12107  dfinfre  12135  infrelb  12139  suprfinzcl  12641  uzwo  12859  supminf  12883  lbzbi  12884  zsupss  12885  suprzcl2  12886  xrsupsslem  13257  xrinfmsslem  13258  xrub  13262  supxr2  13264  supxrun  13266  supxrunb1  13269  supxrbnd1  13271  supxrbnd2  13272  supxrub  13274  supxrbnd  13278  infxrlb  13285  elfzom1elp1fzo  13685  ssfzo12  13712  fsuppmapnn0fiublem  13950  fsuppmapnn0fiub  13951  fsuppmapnn0fiub0  13953  seqsplit  13995  shftlem  15028  rpnnen2lem10  16188  rpnnen2lem11  16189  gcdcllem1  16466  mrcuni  17585  isacs1i  17621  mreacs  17622  lubss  18477  gsumwspan  18812  subgint  19124  cntziinsn  19310  cntzsubg  19312  pmtrdifellem4  19452  subrngint  20539  cntzsubrng  20546  subrgint  20574  cntzsubr  20585  sraassab  21850  mdetunilem9  22610  tgcl  22959  fctop  22994  cctop  22996  neips  23103  cmpsub  23390  1stcelcls  23451  ssref  23502  comppfsc  23522  txbasval  23596  fgss2  23864  filconn  23873  filuni  23875  filssufilg  23901  fmfnfmlem4  23947  trust  24219  elmopn2  24435  metrest  24514  dscopn  24563  metds0  24841  cncfmet  24901  negcncf  24914  iscmet2  25286  ovolfioo  25459  ovolficc  25460  itg1mulc  25696  ply1term  26194  plyconst  26196  reeff1olem  26436  nosupno  27692  nosupbday  27694  nosupbnd1lem5  27701  noinfno  27707  noinfbday  27709  noetasuplem4  27725  n0fincut  28372  usgruspgrb  29277  ocsh  31379  ocorth  31387  spansncvi  31748  pjss1coi  32259  sumdmdii  32511  unidifsnel  32630  dfcnv2  32774  xrge0infss  32859  measdivcst  34415  measdivcstALTV  34416  dya2iocuni  34474  bnj1190  35197  nummin  35281  trssfir1om  35299  trssfir1omregs  35324  opnrebl  36555  opnrebl2  36556  fness  36584  ttcmin  36731  nlpineqsn  37777  fin2so  37981  matunitlindflem1  37990  poimirlem27  38021  poimir  38027  frinfm  38109  filbcmb  38114  nnubfi  38124  nninfnub  38125  sstotbnd3  38150  bndss  38160  exidreslem  38251  isidlc  38389  idlnegcl  38396  intidl  38403  unichnidl  38405  pmapglb2N  40270  elpaddn0  40299  paddasslem9  40327  paddasslem10  40328  pclfinN  40399  polval2N  40405  diaglbN  41554  dihord6apre  41755  unielss  43670  onmaxnelsup  43675  onsupmaxb  43691  onsupeqnmax  43699  gneispace  44585  snsslVD  45279  snssl  45280  sstrALT2VD  45284  sstrALT2  45285  suctrALTcf  45372  suctrALTcfVD  45373  ssnel  45498  uzwo4  45508  infxrunb2  45819  infxrbnd2  45820  supxrunb3  45850  unb2ltle  45865  infxrpnf  45896  supminfxr  45914  sge0iunmptlemfi  46863  caratheodorylem2  46977  ovnlerp  47012  ssfz12  47784  prssspr  47967  prsssprel  47970  lindslinindimp2lem4  48959  lindslinindsimp2  48961  lincresunit3lem2  48978  lincresunit3  48979