Theorem ssel2 3917

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3907

This theorem is referenced by:  tz7.7  6343  onfr  6356  onmindif  6411  ordunisssuc  6425  ssimaex  6919  nssdmovg  7542  onnmin  7745  onmindif2  7754  limsssuc  7794  el2xpss  7983  1st2nd  7985  f1o2ndf1  8065  dfrecs3  8305  boxriin  8881  ordunifi  9193  isfinite2  9201  ordtypelem7  9432  sucprcreg  9512  cnfcom  9612  eldju1st  9838  coflim  10174  cflim2  10176  fin23lem11  10230  fin23lem26  10238  fin1a2lem13  10325  fpwwe2lem11  10555  suplem2pr  10967  axpre-sup  11083  axsup  11212  dedekind  11300  dedekindle  11301  fimaxre  12091  fiminre  12094  lbinf  12100  dfinfre  12128  infrelb  12132  suprfinzcl  12634  uzwo  12852  supminf  12876  lbzbi  12877  zsupss  12878  suprzcl2  12879  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  supxr2  13257  supxrun  13259  supxrunb1  13262  supxrbnd1  13264  supxrbnd2  13265  supxrub  13267  supxrbnd  13271  infxrlb  13278  elfzom1elp1fzo  13678  ssfzo12  13705  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  fsuppmapnn0fiub0  13946  seqsplit  13988  shftlem  15021  rpnnen2lem10  16181  rpnnen2lem11  16182  gcdcllem1  16459  mrcuni  17578  isacs1i  17614  mreacs  17615  lubss  18470  gsumwspan  18805  subgint  19117  cntziinsn  19303  cntzsubg  19305  pmtrdifellem4  19445  subrngint  20528  cntzsubrng  20535  subrgint  20563  cntzsubr  20574  sraassab  21858  mdetunilem9  22595  tgcl  22944  fctop  22979  cctop  22981  neips  23088  cmpsub  23375  1stcelcls  23436  ssref  23487  comppfsc  23507  txbasval  23581  fgss2  23849  filconn  23858  filuni  23860  filssufilg  23886  fmfnfmlem4  23932  trust  24204  elmopn2  24420  metrest  24499  dscopn  24548  metds0  24826  cncfmet  24886  negcncf  24899  iscmet2  25271  ovolfioo  25444  ovolficc  25445  itg1mulc  25681  ply1term  26179  plyconst  26181  reeff1olem  26424  nosupno  27681  nosupbday  27683  nosupbnd1lem5  27690  noinfno  27696  noinfbday  27698  noetasuplem4  27714  n0fincut  28361  usgruspgrb  29266  ocsh  31369  ocorth  31377  spansncvi  31738  pjss1coi  32249  sumdmdii  32501  unidifsnel  32620  dfcnv2  32763  xrge0infss  32848  measdivcst  34384  measdivcstALTV  34385  dya2iocuni  34443  bnj1190  35166  nummin  35252  trssfir1om  35271  trssfir1omregs  35296  opnrebl  36518  opnrebl2  36519  fness  36547  ttcmin  36694  nlpineqsn  37738  fin2so  37942  matunitlindflem1  37951  poimirlem27  37982  poimir  37988  frinfm  38070  filbcmb  38075  nnubfi  38085  nninfnub  38086  sstotbnd3  38111  bndss  38121  exidreslem  38212  isidlc  38350  idlnegcl  38357  intidl  38364  unichnidl  38366  pmapglb2N  40231  elpaddn0  40260  paddasslem9  40288  paddasslem10  40289  pclfinN  40360  polval2N  40366  diaglbN  41515  dihord6apre  41716  unielss  43664  onmaxnelsup  43669  onsupmaxb  43685  onsupeqnmax  43693  gneispace  44579  snsslVD  45273  snssl  45274  sstrALT2VD  45278  sstrALT2  45279  suctrALTcf  45366  suctrALTcfVD  45367  ssnel  45492  uzwo4  45502  infxrunb2  45815  infxrbnd2  45816  supxrunb3  45846  unb2ltle  45861  infxrpnf  45892  supminfxr  45910  sge0iunmptlemfi  46859  caratheodorylem2  46973  ovnlerp  47008  ssfz12  47774  prssspr  47957  prsssprel  47960  lindslinindimp2lem4  48949  lindslinindsimp2  48951  lincresunit3lem2  48968  lincresunit3  48969