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  6332  onfr  6345  onmindif  6400  ordunisssuc  6414  ssimaex  6907  nssdmovg  7528  onnmin  7731  onmindif2  7740  limsssuc  7780  el2xpss  7969  1st2nd  7971  f1o2ndf1  8052  dfrecs3  8292  boxriin  8864  ordunifi  9174  isfinite2  9182  ordtypelem7  9410  sucprcreg  9490  cnfcom  9590  eldju1st  9816  coflim  10152  cflim2  10154  fin23lem11  10208  fin23lem26  10216  fin1a2lem13  10303  fpwwe2lem11  10532  suplem2pr  10944  axpre-sup  11060  axsup  11188  dedekind  11276  dedekindle  11277  fimaxre  12066  fiminre  12069  lbinf  12075  dfinfre  12103  infrelb  12107  suprfinzcl  12587  uzwo  12809  supminf  12833  lbzbi  12834  zsupss  12835  suprzcl2  12836  xrsupsslem  13206  xrinfmsslem  13207  xrub  13211  supxr2  13213  supxrun  13215  supxrunb1  13218  supxrbnd1  13220  supxrbnd2  13221  supxrub  13223  supxrbnd  13227  infxrlb  13234  elfzom1elp1fzo  13632  ssfzo12  13659  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  fsuppmapnn0fiub0  13900  seqsplit  13942  shftlem  14975  rpnnen2lem10  16132  rpnnen2lem11  16133  gcdcllem1  16410  mrcuni  17527  isacs1i  17563  mreacs  17564  lubss  18419  gsumwspan  18754  subgint  19063  cntziinsn  19249  cntzsubg  19251  pmtrdifellem4  19391  subrngint  20475  cntzsubrng  20482  subrgint  20510  cntzsubr  20521  sraassab  21805  mdetunilem9  22535  tgcl  22884  fctop  22919  cctop  22921  neips  23028  cmpsub  23315  1stcelcls  23376  ssref  23427  comppfsc  23447  txbasval  23521  fgss2  23789  filconn  23798  filuni  23800  filssufilg  23826  fmfnfmlem4  23872  trust  24144  elmopn2  24360  metrest  24439  dscopn  24488  metds0  24766  cncfmet  24829  negcncf  24842  negcncfOLD  24843  iscmet2  25221  ovolfioo  25395  ovolficc  25396  itg1mulc  25632  ply1term  26136  plyconst  26138  reeff1olem  26383  nosupno  27642  nosupbday  27644  nosupbnd1lem5  27651  noinfno  27657  noinfbday  27659  noetasuplem4  27675  n0sfincut  28282  usgruspgrb  29161  ocsh  31263  ocorth  31271  spansncvi  31632  pjss1coi  32143  sumdmdii  32395  unidifsnel  32515  dfcnv2  32658  xrge0infss  32743  measdivcst  34237  measdivcstALTV  34238  dya2iocuni  34296  bnj1190  35020  nummin  35104  trssfir1om  35122  trssfir1omregs  35132  opnrebl  36364  opnrebl2  36365  fness  36393  nlpineqsn  37452  fin2so  37657  matunitlindflem1  37666  poimirlem27  37697  poimir  37703  frinfm  37785  filbcmb  37790  nnubfi  37800  nninfnub  37801  sstotbnd3  37826  bndss  37836  exidreslem  37927  isidlc  38065  idlnegcl  38072  intidl  38079  unichnidl  38081  pmapglb2N  39880  elpaddn0  39909  paddasslem9  39937  paddasslem10  39938  pclfinN  40009  polval2N  40015  diaglbN  41164  dihord6apre  41365  unielss  43321  onmaxnelsup  43326  onsupmaxb  43342  onsupeqnmax  43350  gneispace  44237  snsslVD  44931  snssl  44932  sstrALT2VD  44936  sstrALT2  44937  suctrALTcf  45024  suctrALTcfVD  45025  ssnel  45150  uzwo4  45160  infxrunb2  45476  infxrbnd2  45477  supxrunb3  45507  unb2ltle  45523  infxrpnf  45554  supminfxr  45572  sge0iunmptlemfi  46521  caratheodorylem2  46635  ovnlerp  46670  ssfz12  47424  prssspr  47595  prsssprel  47598  lindslinindimp2lem4  48572  lindslinindsimp2  48574  lincresunit3lem2  48591  lincresunit3  48592