Theorem ssel2 3924

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-ss 3914

This theorem is referenced by:  tz7.7  6327  onfr  6340  onmindif  6395  ordunisssuc  6409  ssimaex  6902  nssdmovg  7523  onnmin  7726  onmindif2  7735  limsssuc  7775  el2xpss  7964  1st2nd  7966  f1o2ndf1  8047  dfrecs3  8287  boxriin  8859  ordunifi  9169  isfinite2  9177  ordtypelem7  9405  sucprcreg  9485  cnfcom  9585  eldju1st  9811  coflim  10147  cflim2  10149  fin23lem11  10203  fin23lem26  10211  fin1a2lem13  10298  fpwwe2lem11  10527  suplem2pr  10939  axpre-sup  11055  axsup  11183  dedekind  11271  dedekindle  11272  fimaxre  12061  fiminre  12064  lbinf  12070  dfinfre  12098  infrelb  12102  suprfinzcl  12582  uzwo  12804  supminf  12828  lbzbi  12829  zsupss  12830  suprzcl2  12831  xrsupsslem  13201  xrinfmsslem  13202  xrub  13206  supxr2  13208  supxrun  13210  supxrunb1  13213  supxrbnd1  13215  supxrbnd2  13216  supxrub  13218  supxrbnd  13222  infxrlb  13229  elfzom1elp1fzo  13627  ssfzo12  13654  fsuppmapnn0fiublem  13892  fsuppmapnn0fiub  13893  fsuppmapnn0fiub0  13895  seqsplit  13937  shftlem  14970  rpnnen2lem10  16127  rpnnen2lem11  16128  gcdcllem1  16405  mrcuni  17522  isacs1i  17558  mreacs  17559  lubss  18414  gsumwspan  18749  subgint  19058  cntziinsn  19244  cntzsubg  19246  pmtrdifellem4  19386  subrngint  20470  cntzsubrng  20477  subrgint  20505  cntzsubr  20516  sraassab  21800  mdetunilem9  22530  tgcl  22879  fctop  22914  cctop  22916  neips  23023  cmpsub  23310  1stcelcls  23371  ssref  23422  comppfsc  23442  txbasval  23516  fgss2  23784  filconn  23793  filuni  23795  filssufilg  23821  fmfnfmlem4  23867  trust  24139  elmopn2  24355  metrest  24434  dscopn  24483  metds0  24761  cncfmet  24824  negcncf  24837  negcncfOLD  24838  iscmet2  25216  ovolfioo  25390  ovolficc  25391  itg1mulc  25627  ply1term  26131  plyconst  26133  reeff1olem  26378  nosupno  27637  nosupbday  27639  nosupbnd1lem5  27646  noinfno  27652  noinfbday  27654  noetasuplem4  27670  n0sfincut  28277  usgruspgrb  29156  ocsh  31255  ocorth  31263  spansncvi  31624  pjss1coi  32135  sumdmdii  32387  unidifsnel  32507  dfcnv2  32650  xrge0infss  32735  measdivcst  34229  measdivcstALTV  34230  dya2iocuni  34288  bnj1190  35012  nummin  35096  trssfir1om  35114  trssfir1omregs  35124  opnrebl  36354  opnrebl2  36355  fness  36383  nlpineqsn  37442  fin2so  37647  matunitlindflem1  37656  poimirlem27  37687  poimir  37693  frinfm  37775  filbcmb  37780  nnubfi  37790  nninfnub  37791  sstotbnd3  37816  bndss  37826  exidreslem  37917  isidlc  38055  idlnegcl  38062  intidl  38069  unichnidl  38071  pmapglb2N  39810  elpaddn0  39839  paddasslem9  39867  paddasslem10  39868  pclfinN  39939  polval2N  39945  diaglbN  41094  dihord6apre  41295  unielss  43251  onmaxnelsup  43256  onsupmaxb  43272  onsupeqnmax  43280  gneispace  44167  snsslVD  44861  snssl  44862  sstrALT2VD  44866  sstrALT2  44867  suctrALTcf  44954  suctrALTcfVD  44955  ssnel  45080  uzwo4  45090  infxrunb2  45406  infxrbnd2  45407  supxrunb3  45437  unb2ltle  45453  infxrpnf  45484  supminfxr  45502  sge0iunmptlemfi  46451  caratheodorylem2  46565  ovnlerp  46600  ssfz12  47345  prssspr  47516  prsssprel  47519  lindslinindimp2lem4  48493  lindslinindsimp2  48495  lincresunit3lem2  48512  lincresunit3  48513