Theorem ssel2 3940

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-ss 3930

This theorem is referenced by:  tz7.7  6383  onfr  6397  onmindif  6452  ordunisssuc  6466  ssimaex  6964  nssdmovg  7590  onnmin  7793  onmindif2  7802  limsssuc  7842  el2xpss  8030  1st2nd  8032  f1o2ndf1  8113  dfrecs3  8355  boxriin  8934  ordunifi  9246  isfinite2  9254  ordtypelem7  9482  sucprcregOLD  9565  cnfcom  9665  eldju1st  9905  coflim  10241  cflim2  10243  fin23lem11  10297  fin23lem26  10305  fin1a2lem13  10392  fpwwe2lem11  10622  suplem2pr  11034  axpre-sup  11150  axsup  11281  dedekind  11369  dedekindle  11370  fimaxre  12155  fiminre  12158  lbinf  12164  dfinfre  12192  infrelb  12196  suprfinzcl  12706  uzwo  12931  supminf  12955  lbzbi  12956  zsupss  12957  suprzcl2  12958  xrsupsslem  13329  xrinfmsslem  13330  xrub  13334  supxr2  13336  supxrun  13338  supxrunb1  13341  supxrbnd1  13343  supxrbnd2  13344  supxrub  13346  supxrbnd  13350  infxrlb  13357  elfzom1elp1fzo  13757  ssfzo12  13784  fsuppmapnn0fiublem  14022  fsuppmapnn0fiub  14023  fsuppmapnn0fiub0  14025  seqsplit  14067  shftlem  15101  rpnnen2lem10  16275  rpnnen2lem11  16276  gcdcllem1  16553  mrcuni  17673  isacs1i  17709  mreacs  17710  lubss  18565  gsumwspan  18901  subgint  19213  cntziinsn  19403  cntzsubg  19405  pmtrdifellem4  19545  subrngint  20641  cntzsubrng  20648  subrgint  20676  cntzsubr  20687  sraassab  21983  mdetunilem9  22742  tgcl  23091  fctop  23126  cctop  23128  neips  23235  cmpsub  23522  1stcelcls  23583  ssref  23634  comppfsc  23654  txbasval  23728  fgss2  23996  filconn  24005  filuni  24007  filssufilg  24033  fmfnfmlem4  24079  trust  24351  elmopn2  24567  metrest  24646  dscopn  24695  metds0  24973  cncfmet  25033  negcncf  25046  iscmet2  25418  ovolfioo  25591  ovolficc  25592  itg1mulc  25828  ply1term  26326  plyconst  26328  reeff1olem  26571  nosupno  27829  nosupbday  27831  nosupbnd1lem5  27838  noinfno  27844  noinfbday  27846  noetasuplem4  27862  n0fincut  28510  usgruspgrb  29470  ocsh  31572  ocorth  31580  spansncvi  31941  pjss1coi  32452  sumdmdii  32704  unidifsnel  32818  dfcnv2  32957  xrge0infss  33042  measdivcst  34555  measdivcstALTV  34556  dya2iocuni  34614  bnj1190  35337  nummin  35423  trssfir1om  35443  trssfir1omregs  35468  opnrebl  36716  opnrebl2  36717  fness  36745  ttcmin  36892  nlpineqsn  37937  fin2so  38141  matunitlindflem1  38150  poimirlem27  38181  poimir  38187  frinfm  38269  filbcmb  38274  nnubfi  38284  nninfnub  38285  sstotbnd3  38310  bndss  38320  exidreslem  38411  isidlc  38549  idlnegcl  38556  intidl  38563  unichnidl  38565  pmapglb2N  40430  elpaddn0  40459  paddasslem9  40487  paddasslem10  40488  pclfinN  40559  polval2N  40565  diaglbN  41714  dihord6apre  41915  unielss  43830  onmaxnelsup  43835  onsupmaxb  43851  onsupeqnmax  43859  gneispace  44745  snsslVD  45422  snssl  45423  sstrALT2VD  45427  sstrALT2  45428  suctrALTcf  45515  suctrALTcfVD  45516  ssnel  45648  uzwo4  45658  infxrunb2  45968  infxrbnd2  45969  supxrunb3  45999  unb2ltle  46014  infxrpnf  46045  supminfxr  46063  sge0iunmptlemfi  47012  caratheodorylem2  47126  ovnlerp  47161  ssfz12  47933  prssspr  48116  prsssprel  48119  lindslinindimp2lem4  49119  lindslinindsimp2  49121  lincresunit3lem2  49138  lincresunit3  49139