Theorem ssel2 3926

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2835  df-ss 3916

This theorem is used by:  tz7.7  6383  onfr  6397  onmindif  6452  ordunisssuc  6466  ssimaex  6963  nssdmovg  7596  onnmin  7797  onmindif2  7806  limsssuc  7846  el2xpss  8034  1st2nd  8036  f1o2ndf1  8119  dfrecs3  8361  boxriin  8947  ordunifi  9260  isfinite2  9268  ordtypelem7  9496  sucprcregOLD  9579  cnfcom  9679  eldju1st  9928  coflim  10263  cflim2  10265  fin23lem11  10319  fin23lem26  10327  fin1a2lem13  10414  fpwwe2lem11  10650  suplem2pr  11062  axpre-sup  11178  axsup  11309  dedekind  11397  dedekindle  11398  fimaxre  12183  fiminre  12186  lbinf  12192  dfinfre  12220  infrelb  12224  suprfinzcl  12735  uzwo  12960  supminf  12984  lbzbi  12985  zsupss  12986  suprzcl2  12987  xrsupsslem  13359  xrinfmsslem  13360  xrub  13364  supxr2  13366  supxrun  13368  supxrunb1  13371  supxrbnd1  13373  supxrbnd2  13374  supxrub  13376  supxrbnd  13380  infxrlb  13387  elfzom1elp1fzo  13788  ssfzo12  13815  fsuppmapnn0fiublem  14054  fsuppmapnn0fiub  14055  fsuppmapnn0fiub0  14057  seqsplit  14099  shftlem  15141  rpnnen2lem10  16311  rpnnen2lem11  16312  gcdcllem1  16589  mrcuni  17709  isacs1i  17745  mreacs  17746  lubss  18601  gsumwspan  18955  subgint  19274  cntziinsn  19464  cntzsubg  19466  pmtrdifellem4  19606  subrngint  20722  cntzsubrng  20729  subrgint  20757  cntzsubr  20768  sraassab  22083  mdetunilem9  22842  matunitlindflem1  22901  tgcl  23194  fctop  23229  cctop  23231  neips  23338  cmpsub  23625  1stcelcls  23687  ssref  23738  comppfsc  23758  txbasval  23832  fgss2  24100  filconn  24109  filuni  24111  filssufilg  24137  fmfnfmlem4  24183  trust  24455  elmopn2  24671  metrest  24750  dscopn  24799  metds0  25077  cncfmet  25137  negcncf  25150  iscmet2  25522  ovolfioo  25695  ovolficc  25696  itg1mulc  25932  ply1term  26429  plyconst  26431  reeff1olem  26682  nosupno  27939  nosupbday  27941  nosupbnd1lem5  27948  noinfno  27954  noinfbday  27956  noetasuplem4  27972  n0fincut  28620  usgruspgrb  29643  ocsh  31764  ocorth  31772  spansncvi  32133  pjss1coi  32644  sumdmdii  32896  unidifsnel  33010  dfcnv2  33148  xrge0infss  33231  measdivcst  34735  measdivcstALTV  34736  dya2iocuni  34794  bnj1190  35517  nummin  35598  trssfir1om  35621  trssfir1omregs  35662  opnrebl  36939  opnrebl2  36940  fness  36968  ttcmin  37115  nlpineqsn  38162  fin2so  38361  poimirlem27  38396  poimir  38402  frinfm  38485  filbcmb  38490  nnubfi  38500  nninfnub  38501  sstotbnd3  38526  bndss  38536  exidreslem  38627  isidlc  38765  idlnegcl  38772  intidl  38779  unichnidl  38781  pmapglb2N  40644  elpaddn0  40673  paddasslem9  40701  paddasslem10  40702  pclfinN  40773  polval2N  40779  diaglbN  41928  dihord6apre  42129  unielss  44059  onmaxnelsup  44064  onsupmaxb  44080  onsupeqnmax  44088  gneispace  44974  snsslVD  45651  snssl  45652  sstrALT2VD  45656  sstrALT2  45657  suctrALTcf  45744  suctrALTcfVD  45745  ssnel  45877  uzwo4  45887  infxrunb2  46197  infxrbnd2  46198  supxrunb3  46228  unb2ltle  46243  infxrpnf  46274  supminfxr  46292  sge0iunmptlemfi  47241  caratheodorylem2  47355  ovnlerp  47390  ssfz12  48202  prssspr  48385  prsssprel  48388  lindslinindimp2lem4  49391  lindslinindsimp2  49393  lincresunit3lem2  49410  lincresunit3  49411