Theorem ssel2 3928

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3901

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 2115

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

This theorem is referenced by:  tz7.7  6343  onfr  6356  onmindif  6411  ordunisssuc  6425  ssimaex  6919  nssdmovg  7540  onnmin  7743  onmindif2  7752  limsssuc  7792  el2xpss  7981  1st2nd  7983  f1o2ndf1  8064  dfrecs3  8304  boxriin  8878  ordunifi  9190  isfinite2  9198  ordtypelem7  9429  sucprcreg  9509  cnfcom  9609  eldju1st  9835  coflim  10171  cflim2  10173  fin23lem11  10227  fin23lem26  10235  fin1a2lem13  10322  fpwwe2lem11  10552  suplem2pr  10964  axpre-sup  11080  axsup  11208  dedekind  11296  dedekindle  11297  fimaxre  12086  fiminre  12089  lbinf  12095  dfinfre  12123  infrelb  12127  suprfinzcl  12606  uzwo  12824  supminf  12848  lbzbi  12849  zsupss  12850  suprzcl2  12851  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  supxr2  13229  supxrun  13231  supxrunb1  13234  supxrbnd1  13236  supxrbnd2  13237  supxrub  13239  supxrbnd  13243  infxrlb  13250  elfzom1elp1fzo  13648  ssfzo12  13675  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  fsuppmapnn0fiub0  13916  seqsplit  13958  shftlem  14991  rpnnen2lem10  16148  rpnnen2lem11  16149  gcdcllem1  16426  mrcuni  17544  isacs1i  17580  mreacs  17581  lubss  18436  gsumwspan  18771  subgint  19080  cntziinsn  19266  cntzsubg  19268  pmtrdifellem4  19408  subrngint  20493  cntzsubrng  20500  subrgint  20528  cntzsubr  20539  sraassab  21823  mdetunilem9  22564  tgcl  22913  fctop  22948  cctop  22950  neips  23057  cmpsub  23344  1stcelcls  23405  ssref  23456  comppfsc  23476  txbasval  23550  fgss2  23818  filconn  23827  filuni  23829  filssufilg  23855  fmfnfmlem4  23901  trust  24173  elmopn2  24389  metrest  24468  dscopn  24517  metds0  24795  cncfmet  24858  negcncf  24871  negcncfOLD  24872  iscmet2  25250  ovolfioo  25424  ovolficc  25425  itg1mulc  25661  ply1term  26165  plyconst  26167  reeff1olem  26412  nosupno  27671  nosupbday  27673  nosupbnd1lem5  27680  noinfno  27686  noinfbday  27688  noetasuplem4  27704  n0fincut  28351  usgruspgrb  29256  ocsh  31358  ocorth  31366  spansncvi  31727  pjss1coi  32238  sumdmdii  32490  unidifsnel  32610  dfcnv2  32754  xrge0infss  32840  measdivcst  34381  measdivcstALTV  34382  dya2iocuni  34440  bnj1190  35164  nummin  35249  trssfir1om  35267  trssfir1omregs  35292  opnrebl  36514  opnrebl2  36515  fness  36543  nlpineqsn  37613  fin2so  37808  matunitlindflem1  37817  poimirlem27  37848  poimir  37854  frinfm  37936  filbcmb  37941  nnubfi  37951  nninfnub  37952  sstotbnd3  37977  bndss  37987  exidreslem  38078  isidlc  38216  idlnegcl  38223  intidl  38230  unichnidl  38232  pmapglb2N  40031  elpaddn0  40060  paddasslem9  40088  paddasslem10  40089  pclfinN  40160  polval2N  40166  diaglbN  41315  dihord6apre  41516  unielss  43460  onmaxnelsup  43465  onsupmaxb  43481  onsupeqnmax  43489  gneispace  44375  snsslVD  45069  snssl  45070  sstrALT2VD  45074  sstrALT2  45075  suctrALTcf  45162  suctrALTcfVD  45163  ssnel  45288  uzwo4  45298  infxrunb2  45612  infxrbnd2  45613  supxrunb3  45643  unb2ltle  45659  infxrpnf  45690  supminfxr  45708  sge0iunmptlemfi  46657  caratheodorylem2  46771  ovnlerp  46806  ssfz12  47560  prssspr  47731  prsssprel  47734  lindslinindimp2lem4  48707  lindslinindsimp2  48709  lincresunit3lem2  48726  lincresunit3  48727