Theorem ssel2 3912

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  tz7.7  6277  onfr  6290  onmindif  6340  ordunisssuc  6353  ssimaex  6835  nssdmovg  7432  onnmin  7625  onmindif2  7634  limsssuc  7672  1st2nd  7853  f1o2ndf1  7934  dfrecs3  8174  dfrecs3OLD  8175  boxriin  8686  ordunifi  8994  isfinite2  9002  ordtypelem7  9213  sucprcreg  9290  cnfcom  9388  eldju1st  9612  coflim  9948  cflim2  9950  fin23lem11  10004  fin23lem26  10012  fin1a2lem13  10099  fpwwe2lem11  10328  suplem2pr  10740  axpre-sup  10856  axsup  10981  dedekind  11068  dedekindle  11069  fimaxre  11849  fiminre  11852  lbinf  11858  dfinfre  11886  infrelb  11890  suprfinzcl  12365  uzwo  12580  supminf  12604  lbzbi  12605  zsupss  12606  suprzcl2  12607  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  supxr2  12977  supxrun  12979  supxrunb1  12982  supxrbnd1  12984  supxrbnd2  12985  supxrub  12987  supxrbnd  12991  infxrlb  12997  elfzom1elp1fzo  13382  ssfzo12  13408  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  fsuppmapnn0fiub0  13641  seqsplit  13684  shftlem  14707  rpnnen2lem10  15860  rpnnen2lem11  15861  gcdcllem1  16134  mrcuni  17247  isacs1i  17283  mreacs  17284  lubss  18146  gsumwspan  18400  subgint  18694  cntziinsn  18856  cntzsubg  18858  pmtrdifellem4  19002  subrgint  19961  cntzsubr  19972  mdetunilem9  21677  tgcl  22027  fctop  22062  cctop  22064  neips  22172  cmpsub  22459  1stcelcls  22520  ssref  22571  comppfsc  22591  txbasval  22665  fgss2  22933  filconn  22942  filuni  22944  filssufilg  22970  fmfnfmlem4  23016  trust  23289  elmopn2  23506  metrest  23586  dscopn  23635  metds0  23919  cncfmet  23978  negcncf  23991  iscmet2  24363  ovolfioo  24536  ovolficc  24537  itg1mulc  24774  ply1term  25270  plyconst  25272  reeff1olem  25510  usgruspgrb  27454  ocsh  29546  ocorth  29554  spansncvi  29915  pjss1coi  30426  sumdmdii  30678  unidifsnel  30784  dfcnv2  30915  xrge0infss  30985  measdivcst  32092  measdivcstALTV  32093  dya2iocuni  32150  bnj1190  32888  nummin  32963  elxpxpss  33587  nosupno  33833  nosupbday  33835  nosupbnd1lem5  33842  noinfno  33848  noinfbday  33850  noetasuplem4  33866  opnrebl  34436  opnrebl2  34437  fness  34465  nlpineqsn  35506  fin2so  35691  matunitlindflem1  35700  poimirlem27  35731  poimir  35737  frinfm  35820  filbcmb  35825  nnubfi  35835  nninfnub  35836  sstotbnd3  35861  bndss  35871  exidreslem  35962  isidlc  36100  idlnegcl  36107  intidl  36114  unichnidl  36116  pmapglb2N  37712  elpaddn0  37741  paddasslem9  37769  paddasslem10  37770  pclfinN  37841  polval2N  37847  diaglbN  38996  dihord6apre  39197  gneispace  41633  snsslVD  42338  snssl  42339  sstrALT2VD  42343  sstrALT2  42344  suctrALTcf  42431  suctrALTcfVD  42432  ssnel  42477  uzwo4  42490  infxrunb2  42797  infxrbnd2  42798  supxrunb3  42829  unb2ltle  42845  infxrpnf  42876  supminfxr  42894  sge0iunmptlemfi  43841  caratheodorylem2  43955  ovnlerp  43990  ssfz12  44694  prssspr  44825  prsssprel  44828  lindslinindimp2lem4  45690  lindslinindsimp2  45692  lincresunit3lem2  45709  lincresunit3  45710