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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  tz7.7  6296  onfr  6309  onmindif  6359  ordunisssuc  6372  ssimaex  6862  nssdmovg  7463  onnmin  7657  onmindif2  7666  limsssuc  7706  1st2nd  7889  f1o2ndf1  7972  dfrecs3  8212  dfrecs3OLD  8213  boxriin  8737  ordunifi  9073  isfinite2  9081  ordtypelem7  9292  sucprcreg  9369  cnfcom  9467  eldju1st  9690  coflim  10026  cflim2  10028  fin23lem11  10082  fin23lem26  10090  fin1a2lem13  10177  fpwwe2lem11  10406  suplem2pr  10818  axpre-sup  10934  axsup  11059  dedekind  11147  dedekindle  11148  fimaxre  11928  fiminre  11931  lbinf  11937  dfinfre  11965  infrelb  11969  suprfinzcl  12445  uzwo  12660  supminf  12684  lbzbi  12685  zsupss  12686  suprzcl2  12687  xrsupsslem  13050  xrinfmsslem  13051  xrub  13055  supxr2  13057  supxrun  13059  supxrunb1  13062  supxrbnd1  13064  supxrbnd2  13065  supxrub  13067  supxrbnd  13071  infxrlb  13077  elfzom1elp1fzo  13463  ssfzo12  13489  fsuppmapnn0fiublem  13719  fsuppmapnn0fiub  13720  fsuppmapnn0fiub0  13722  seqsplit  13765  shftlem  14788  rpnnen2lem10  15941  rpnnen2lem11  15942  gcdcllem1  16215  mrcuni  17339  isacs1i  17375  mreacs  17376  lubss  18240  gsumwspan  18494  subgint  18788  cntziinsn  18950  cntzsubg  18952  pmtrdifellem4  19096  subrgint  20055  cntzsubr  20066  mdetunilem9  21778  tgcl  22128  fctop  22163  cctop  22165  neips  22273  cmpsub  22560  1stcelcls  22621  ssref  22672  comppfsc  22692  txbasval  22766  fgss2  23034  filconn  23043  filuni  23045  filssufilg  23071  fmfnfmlem4  23117  trust  23390  elmopn2  23607  metrest  23689  dscopn  23738  metds0  24022  cncfmet  24081  negcncf  24094  iscmet2  24467  ovolfioo  24640  ovolficc  24641  itg1mulc  24878  ply1term  25374  plyconst  25376  reeff1olem  25614  usgruspgrb  27560  ocsh  29654  ocorth  29662  spansncvi  30023  pjss1coi  30534  sumdmdii  30786  unidifsnel  30892  dfcnv2  31022  xrge0infss  31092  measdivcst  32201  measdivcstALTV  32202  dya2iocuni  32259  bnj1190  32997  nummin  33072  elxpxpss  33693  nosupno  33915  nosupbday  33917  nosupbnd1lem5  33924  noinfno  33930  noinfbday  33932  noetasuplem4  33948  opnrebl  34518  opnrebl2  34519  fness  34547  nlpineqsn  35588  fin2so  35773  matunitlindflem1  35782  poimirlem27  35813  poimir  35819  frinfm  35902  filbcmb  35907  nnubfi  35917  nninfnub  35918  sstotbnd3  35943  bndss  35953  exidreslem  36044  isidlc  36182  idlnegcl  36189  intidl  36196  unichnidl  36198  pmapglb2N  37792  elpaddn0  37821  paddasslem9  37849  paddasslem10  37850  pclfinN  37921  polval2N  37927  diaglbN  39076  dihord6apre  39277  gneispace  41751  snsslVD  42456  snssl  42457  sstrALT2VD  42461  sstrALT2  42462  suctrALTcf  42549  suctrALTcfVD  42550  ssnel  42595  uzwo4  42608  infxrunb2  42914  infxrbnd2  42915  supxrunb3  42946  unb2ltle  42962  infxrpnf  42993  supminfxr  43011  sge0iunmptlemfi  43958  caratheodorylem2  44072  ovnlerp  44107  ssfz12  44817  prssspr  44948  prsssprel  44951  lindslinindimp2lem4  45813  lindslinindsimp2  45815  lincresunit3lem2  45832  lincresunit3  45833