Theorem ssel2 3598

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

Assertion

Ref	Expression
ssel2	|- ( ( A C_ B /\ C e. A ) -> C e. B )

Proof of Theorem ssel2

Step	Hyp	Ref	Expression
1		ssel 3597	. 2 |- ( A C_ B -> ( C e. A -> C e. B ) )
2	1	imp 445	1 |- ( ( A C_ B /\ C e. A ) -> C e. B )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  tz7.7  5749  onfr  5763  onmindif  5815  ordunisssuc  5830  ssimaex  6263  nssdmovg  6816  onnmin  7003  onmindif2  7012  limsssuc  7050  1st2nd  7214  f1o2ndf1  7285  dfrecs3  7469  boxriin  7950  ordunifi  8210  isfinite2  8218  ordtypelem7  8429  sucprcreg  8506  cnfcom  8597  coflim  9083  cflim2  9085  fin23lem11  9139  fin23lem26  9147  fin1a2lem13  9234  fpwwe2lem12  9463  suplem2pr  9875  axpre-sup  9990  axsup  10113  dedekind  10200  dedekindle  10201  lbinf  10976  dfinfre  11004  infrelb  11008  suprfinzcl  11492  uzwo  11751  supminf  11775  lbzbi  11776  zsupss  11777  suprzcl2  11778  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxr2  12144  supxrun  12146  supxrunb1  12149  supxrbnd1  12151  supxrbnd2  12152  supxrub  12154  supxrbnd  12158  infxrlb  12164  elfzom1elp1fzo  12534  ssfzo12  12561  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  fsuppmapnn0fiub0  12793  seqsplit  12834  shftlem  13808  rpnnen2lem10  14952  rpnnen2lem11  14953  gcdcllem1  15221  mrcuni  16281  isacs1i  16318  mreacs  16319  lubss  17121  gsumwspan  17383  subgint  17618  cntziinsn  17767  cntzsubg  17769  pmtrdifellem4  17899  subrgint  18802  cntzsubr  18812  mdetunilem9  20426  tgcl  20773  fctop  20808  cctop  20810  neips  20917  cmpsub  21203  1stcelcls  21264  ssref  21315  comppfsc  21335  txbasval  21409  fgss2  21678  filconn  21687  filuni  21689  filssufilg  21715  fmfnfmlem4  21761  trust  22033  elmopn2  22250  metrest  22329  dscopn  22378  metds0  22653  cncfmet  22711  negcncf  22721  iscmet2  23092  ovolfioo  23236  ovolficc  23237  itg1mulc  23471  ply1term  23960  plyconst  23962  reeff1olem  24200  usgruspgrb  26076  ocsh  28142  ocorth  28150  spansncvi  28511  pjss1coi  29022  sumdmdii  29274  dfcnv2  29476  xrge0infss  29525  measres  30285  measdivcstOLD  30287  measdivcst  30288  dya2iocuni  30345  bnj1190  31076  elintfv  31662  frrlem5e  31788  nosupno  31849  nosupbday  31851  nosupbnd1lem5  31858  noetalem3  31865  opnrebl  32315  opnrebl2  32316  fness  32344  fin2so  33396  matunitlindflem1  33405  poimirlem27  33436  poimir  33442  frinfm  33530  filbcmb  33535  nnubfi  33546  nninfnub  33547  sstotbnd3  33575  bndss  33585  exidreslem  33676  isidlc  33814  idlnegcl  33821  intidl  33828  unichnidl  33830  pmapglb2N  35057  elpaddn0  35086  paddasslem9  35114  paddasslem10  35115  pclfinN  35186  polval2N  35192  diaglbN  36344  dihord6apre  36545  gneispace  38432  snsslVD  39064  snssl  39065  sstrALT2VD  39069  sstrALT2  39070  suctrALTcf  39158  suctrALTcfVD  39159  ssnel  39204  uzwo4  39221  infxrunb2  39584  infxrbnd2  39585  supxrunb3  39623  unb2ltle  39642  infxrpnf  39674  supminfxr  39694  sge0iunmptlemfi  40630  caratheodorylem2  40741  ovnlerp  40776  ssfz12  41324  prssspr  41735  prsssprel  41738  lindslinindimp2lem4  42250  lindslinindsimp2  42252  lincresunit3lem2  42269  lincresunit3  42270