Theorem ssel2 3977

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 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clel 2815  df-ss 3967

This theorem is referenced by:  tz7.7  6409  onfr  6422  onmindif  6475  ordunisssuc  6489  ssimaex  6993  nssdmovg  7616  onnmin  7819  onmindif2  7828  limsssuc  7872  el2xpss  8063  1st2nd  8065  f1o2ndf1  8148  dfrecs3  8413  dfrecs3OLD  8414  boxriin  8981  ordunifi  9327  isfinite2  9335  ordtypelem7  9565  sucprcreg  9642  cnfcom  9741  eldju1st  9964  coflim  10302  cflim2  10304  fin23lem11  10358  fin23lem26  10366  fin1a2lem13  10453  fpwwe2lem11  10682  suplem2pr  11094  axpre-sup  11210  axsup  11337  dedekind  11425  dedekindle  11426  fimaxre  12213  fiminre  12216  lbinf  12222  dfinfre  12250  infrelb  12254  suprfinzcl  12734  uzwo  12954  supminf  12978  lbzbi  12979  zsupss  12980  suprzcl2  12981  xrsupsslem  13350  xrinfmsslem  13351  xrub  13355  supxr2  13357  supxrun  13359  supxrunb1  13362  supxrbnd1  13364  supxrbnd2  13365  supxrub  13367  supxrbnd  13371  infxrlb  13377  elfzom1elp1fzo  13772  ssfzo12  13799  fsuppmapnn0fiublem  14032  fsuppmapnn0fiub  14033  fsuppmapnn0fiub0  14035  seqsplit  14077  shftlem  15108  rpnnen2lem10  16260  rpnnen2lem11  16261  gcdcllem1  16537  mrcuni  17665  isacs1i  17701  mreacs  17702  lubss  18559  gsumwspan  18860  subgint  19169  cntziinsn  19356  cntzsubg  19358  pmtrdifellem4  19498  subrngint  20561  cntzsubrng  20568  subrgint  20596  cntzsubr  20607  sraassab  21889  mdetunilem9  22627  tgcl  22977  fctop  23012  cctop  23014  neips  23122  cmpsub  23409  1stcelcls  23470  ssref  23521  comppfsc  23541  txbasval  23615  fgss2  23883  filconn  23892  filuni  23894  filssufilg  23920  fmfnfmlem4  23966  trust  24239  elmopn2  24456  metrest  24538  dscopn  24587  metds0  24873  cncfmet  24936  negcncf  24949  negcncfOLD  24950  iscmet2  25329  ovolfioo  25503  ovolficc  25504  itg1mulc  25740  ply1term  26244  plyconst  26246  reeff1olem  26491  nosupno  27749  nosupbday  27751  nosupbnd1lem5  27758  noinfno  27764  noinfbday  27766  noetasuplem4  27782  usgruspgrb  29201  ocsh  31303  ocorth  31311  spansncvi  31672  pjss1coi  32183  sumdmdii  32435  unidifsnel  32554  dfcnv2  32687  xrge0infss  32765  measdivcst  34226  measdivcstALTV  34227  dya2iocuni  34286  bnj1190  35023  nummin  35106  opnrebl  36322  opnrebl2  36323  fness  36351  nlpineqsn  37410  fin2so  37615  matunitlindflem1  37624  poimirlem27  37655  poimir  37661  frinfm  37743  filbcmb  37748  nnubfi  37758  nninfnub  37759  sstotbnd3  37784  bndss  37794  exidreslem  37885  isidlc  38023  idlnegcl  38030  intidl  38037  unichnidl  38039  pmapglb2N  39774  elpaddn0  39803  paddasslem9  39831  paddasslem10  39832  pclfinN  39903  polval2N  39909  diaglbN  41058  dihord6apre  41259  unielss  43235  onmaxnelsup  43240  onsupmaxb  43256  onsupeqnmax  43264  gneispace  44152  snsslVD  44854  snssl  44855  sstrALT2VD  44859  sstrALT2  44860  suctrALTcf  44947  suctrALTcfVD  44948  ssnel  45053  uzwo4  45063  infxrunb2  45384  infxrbnd2  45385  supxrunb3  45415  unb2ltle  45431  infxrpnf  45462  supminfxr  45480  sge0iunmptlemfi  46433  caratheodorylem2  46547  ovnlerp  46582  ssfz12  47331  prssspr  47477  prsssprel  47480  lindslinindimp2lem4  48383  lindslinindsimp2  48385  lincresunit3lem2  48402  lincresunit3  48403