Theorem ssel2 3938

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3928

This theorem is referenced by:  tz7.7  6346  onfr  6359  onmindif  6414  ordunisssuc  6428  ssimaex  6928  nssdmovg  7551  onnmin  7754  onmindif2  7763  limsssuc  7806  el2xpss  7995  1st2nd  7997  f1o2ndf1  8078  dfrecs3  8318  boxriin  8890  ordunifi  9213  isfinite2  9221  ordtypelem7  9453  sucprcreg  9530  cnfcom  9629  eldju1st  9852  coflim  10190  cflim2  10192  fin23lem11  10246  fin23lem26  10254  fin1a2lem13  10341  fpwwe2lem11  10570  suplem2pr  10982  axpre-sup  11098  axsup  11225  dedekind  11313  dedekindle  11314  fimaxre  12103  fiminre  12106  lbinf  12112  dfinfre  12140  infrelb  12144  suprfinzcl  12624  uzwo  12846  supminf  12870  lbzbi  12871  zsupss  12872  suprzcl2  12873  xrsupsslem  13243  xrinfmsslem  13244  xrub  13248  supxr2  13250  supxrun  13252  supxrunb1  13255  supxrbnd1  13257  supxrbnd2  13258  supxrub  13260  supxrbnd  13264  infxrlb  13271  elfzom1elp1fzo  13669  ssfzo12  13696  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  fsuppmapnn0fiub0  13934  seqsplit  13976  shftlem  15010  rpnnen2lem10  16167  rpnnen2lem11  16168  gcdcllem1  16445  mrcuni  17558  isacs1i  17594  mreacs  17595  lubss  18448  gsumwspan  18749  subgint  19058  cntziinsn  19245  cntzsubg  19247  pmtrdifellem4  19385  subrngint  20445  cntzsubrng  20452  subrgint  20480  cntzsubr  20491  sraassab  21753  mdetunilem9  22483  tgcl  22832  fctop  22867  cctop  22869  neips  22976  cmpsub  23263  1stcelcls  23324  ssref  23375  comppfsc  23395  txbasval  23469  fgss2  23737  filconn  23746  filuni  23748  filssufilg  23774  fmfnfmlem4  23820  trust  24093  elmopn2  24309  metrest  24388  dscopn  24437  metds0  24715  cncfmet  24778  negcncf  24791  negcncfOLD  24792  iscmet2  25170  ovolfioo  25344  ovolficc  25345  itg1mulc  25581  ply1term  26085  plyconst  26087  reeff1olem  26332  nosupno  27591  nosupbday  27593  nosupbnd1lem5  27600  noinfno  27606  noinfbday  27608  noetasuplem4  27624  n0sfincut  28222  usgruspgrb  29086  ocsh  31185  ocorth  31193  spansncvi  31554  pjss1coi  32065  sumdmdii  32317  unidifsnel  32437  dfcnv2  32573  xrge0infss  32656  measdivcst  34187  measdivcstALTV  34188  dya2iocuni  34247  bnj1190  34971  nummin  35054  opnrebl  36281  opnrebl2  36282  fness  36310  nlpineqsn  37369  fin2so  37574  matunitlindflem1  37583  poimirlem27  37614  poimir  37620  frinfm  37702  filbcmb  37707  nnubfi  37717  nninfnub  37718  sstotbnd3  37743  bndss  37753  exidreslem  37844  isidlc  37982  idlnegcl  37989  intidl  37996  unichnidl  37998  pmapglb2N  39738  elpaddn0  39767  paddasslem9  39795  paddasslem10  39796  pclfinN  39867  polval2N  39873  diaglbN  41022  dihord6apre  41223  unielss  43180  onmaxnelsup  43185  onsupmaxb  43201  onsupeqnmax  43209  gneispace  44096  snsslVD  44791  snssl  44792  sstrALT2VD  44796  sstrALT2  44797  suctrALTcf  44884  suctrALTcfVD  44885  ssnel  45010  uzwo4  45020  infxrunb2  45337  infxrbnd2  45338  supxrunb3  45368  unb2ltle  45384  infxrpnf  45415  supminfxr  45433  sge0iunmptlemfi  46384  caratheodorylem2  46498  ovnlerp  46533  ssfz12  47288  prssspr  47459  prsssprel  47462  lindslinindimp2lem4  48423  lindslinindsimp2  48425  lincresunit3lem2  48442  lincresunit3  48443