Theorem ssel2 3908

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-ss 3901

This theorem is used by:  frinf  6316  tz7.7  6414  onfr  6428  onmindif  6483  ordunisssuc  6497  ssimaex  7001  nssdmovg  7635  onnmin  7846  onmindif2  7855  limsssuc  7895  el2xpss  8082  1st2nd  8084  f1o2ndf1  8170  dfrecs3  8418  onelfvnef1  8487  boxriin  9006  ordunifi  9319  isfinite2  9328  ordtypelem7  9555  sucprcregOLD  9638  cnfcom  9738  elhf3OLD  9960  eldju1st  10041  coflim  10378  cflim2  10380  fin23lem11  10434  fin23lem26  10442  fin1a2lem13  10529  fpwwe2lem11  10765  suplem2pr  11177  axpre-sup  11293  axsup  11424  dedekind  11512  dedekindle  11513  fimaxre  12301  fiminre  12304  lbinf  12310  dfinfre  12338  infrelb  12342  suprfinzcl  12853  uzwo  13078  supminf  13102  lbzbi  13103  zsupss  13104  suprzcl2  13105  xrsupsslem  13477  xrinfmsslem  13478  xrub  13482  supxr2  13484  supxrun  13486  supxrunb1  13489  supxrbnd1  13491  supxrbnd2  13492  supxrub  13494  supxrbnd  13498  infxrlb  13505  elfzom1elp1fzo  13907  ssfzo12  13934  fsuppmapnn0fiublem  14173  fsuppmapnn0fiub  14174  fsuppmapnn0fiub0  14176  seqsplit  14218  shftlem  15264  rpnnen2lem10  16435  rpnnen2lem11  16436  gcdcllem1  16713  mrcuni  17845  isacs1i  17881  mreacs  17882  lubss  18737  gsumwspan  19092  subgint  19411  cntziinsn  19602  cntzsubg  19604  pmtrdifellem4  19744  subrngint  20863  cntzsubrng  20870  subrgint  20898  cntzsubr  20909  sraassab  22231  mdetunilem9  22990  matunitlindflem1  23049  tgcl  23342  fctop  23377  cctop  23379  neips  23486  cmpsub  23773  1stcelcls  23835  ssref  23886  comppfsc  23906  txbasval  23980  fgss2  24248  filconn  24257  filuni  24259  filssufilg  24285  fmfnfmlem4  24331  trust  24603  elmopn2  24819  metrest  24898  dscopn  24947  metds0  25225  cncfmet  25285  negcncf  25298  iscmet2  25670  ovolfioo  25843  ovolficc  25844  itg1mulc  26080  ply1term  26577  plyconst  26579  reeff1olem  26830  nosupno  28117  nosupbday  28119  nosupbnd1lem5  28126  noinfno  28132  noinfbday  28134  noetasuplem4  28150  n0fincut  28798  usgruspgrb  29821  ocsh  31942  ocorth  31950  spansncvi  32311  pjss1coi  32822  sumdmdii  33074  unidifsnel  33229  dfcnv2  33366  xrge0infss  33448  measdivcst  34968  measdivcstALTV  34969  dya2iocuni  35026  bnj1190  35749  nummin  35847  trssfihf  35860  trssfihfregs  35945  onprcf1acwevdlem1  36086  opnrebl  37323  opnrebl2  37324  fness  37352  ttcmin  37499  nlpineqsn  38599  fin2so  38798  poimirlem27  38833  poimir  38839  filbcmb  38940  nnubfi  38950  nninfnub  38951  sstotbnd3  38976  bndss  38986  exidreslem  39077  isidlc  39215  idlnegcl  39222  intidl  39229  unichnidl  39231  pmapglb2N  41094  elpaddn0  41123  paddasslem9  41151  paddasslem10  41152  pclfinN  41223  polval2N  41229  diaglbN  42378  dihord6apre  42579  unielss  44481  onmaxnelsup  44486  onsupmaxb  44502  onsupeqnmax  44510  gneispace  45395  snsslVD  46071  snssl  46072  sstrALT2VD  46076  sstrALT2  46077  suctrALTcf  46164  suctrALTcfVD  46165  ssnel  46334  uzwo4  46344  infxrunb2  46652  infxrbnd2  46653  supxrunb3  46683  unb2ltle  46698  infxrpnf  46729  supminfxr  46747  sge0iunmptlemfi  47696  caratheodorylem2  47810  ovnlerp  47845  ssfz12  48657  prssspr  48840  prsssprel  48843  lindslinindimp2lem4  49904  lindslinindsimp2  49906  lincresunit3lem2  49923  lincresunit3  49924