Theorem ssel2 3787

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2155   ⊆ wss 3763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-in 3770  df-ss 3777

This theorem is referenced by:  tz7.7  5956  onfr  5970  onmindif  6022  ordunisssuc  6037  ssimaex  6478  nssdmovg  7040  onnmin  7227  onmindif2  7236  limsssuc  7274  1st2nd  7440  f1o2ndf1  7513  dfrecs3  7699  boxriin  8181  ordunifi  8443  isfinite2  8451  ordtypelem7  8662  sucprcreg  8739  cnfcom  8838  eldju1st  9026  coflim  9362  cflim2  9364  fin23lem11  9418  fin23lem26  9426  fin1a2lem13  9513  fpwwe2lem12  9742  suplem2pr  10154  axpre-sup  10269  axsup  10392  dedekind  10479  dedekindle  10480  lbinf  11255  dfinfre  11283  infrelb  11287  suprfinzcl  11752  uzwo  11964  supminf  11988  lbzbi  11989  zsupss  11990  suprzcl2  11991  xrsupsslem  12349  xrinfmsslem  12350  xrub  12354  supxr2  12356  supxrun  12358  supxrunb1  12361  supxrbnd1  12363  supxrbnd2  12364  supxrub  12366  supxrbnd  12370  infxrlb  12376  elfzom1elp1fzo  12753  ssfzo12  12779  fsuppmapnn0fiublem  13007  fsuppmapnn0fiub  13008  fsuppmapnn0fiub0  13010  seqsplit  13051  shftlem  14025  rpnnen2lem10  15166  rpnnen2lem11  15167  gcdcllem1  15434  mrcuni  16480  isacs1i  16516  mreacs  16517  lubss  17320  gsumwspan  17582  subgint  17814  cntziinsn  17962  cntzsubg  17964  pmtrdifellem4  18094  subrgint  19000  cntzsubr  19010  mdetunilem9  20631  tgcl  20981  fctop  21016  cctop  21018  neips  21125  cmpsub  21411  1stcelcls  21472  ssref  21523  comppfsc  21543  txbasval  21617  fgss2  21885  filconn  21894  filuni  21896  filssufilg  21922  fmfnfmlem4  21968  trust  22240  elmopn2  22457  metrest  22536  dscopn  22585  metds0  22860  cncfmet  22918  negcncf  22928  iscmet2  23298  ovolfioo  23442  ovolficc  23443  itg1mulc  23679  ply1term  24168  plyconst  24170  reeff1olem  24408  usgruspgrb  26285  ocsh  28464  ocorth  28472  spansncvi  28833  pjss1coi  29344  sumdmdii  29596  dfcnv2  29797  xrge0infss  29846  measres  30604  measdivcstOLD  30606  measdivcst  30607  dya2iocuni  30664  bnj1190  31393  elintfv  31978  frrlem5e  32103  nosupno  32164  nosupbday  32166  nosupbnd1lem5  32173  noetalem3  32180  opnrebl  32630  opnrebl2  32631  fness  32659  fin2so  33703  matunitlindflem1  33712  poimirlem27  33743  poimir  33749  frinfm  33836  filbcmb  33841  nnubfi  33851  nninfnub  33852  sstotbnd3  33880  bndss  33890  exidreslem  33981  isidlc  34119  idlnegcl  34126  intidl  34133  unichnidl  34135  pmapglb2N  35545  elpaddn0  35574  paddasslem9  35602  paddasslem10  35603  pclfinN  35674  polval2N  35680  diaglbN  36830  dihord6apre  37031  gneispace  38926  snsslVD  39552  snssl  39553  sstrALT2VD  39557  sstrALT2  39558  suctrALTcf  39646  suctrALTcfVD  39647  ssnel  39692  uzwo4  39708  infxrunb2  40058  infxrbnd2  40059  supxrunb3  40096  unb2ltle  40115  infxrpnf  40147  supminfxr  40167  sge0iunmptlemfi  41103  caratheodorylem2  41217  ovnlerp  41252  ssfz12  41893  prssspr  42297  prsssprel  42300  lindslinindimp2lem4  42812  lindslinindsimp2  42814  lincresunit3lem2  42831  lincresunit3  42832