Theorem ssel2 3974

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-clel 2803  df-ss 3964

This theorem is referenced by:  tz7.7  6402  onfr  6415  onmindif  6468  ordunisssuc  6482  ssimaex  6987  nssdmovg  7608  onnmin  7807  onmindif2  7816  limsssuc  7860  el2xpss  8051  1st2nd  8053  f1o2ndf1  8136  dfrecs3  8402  dfrecs3OLD  8403  boxriin  8969  ordunifi  9327  isfinite2  9335  ordtypelem7  9567  sucprcreg  9644  cnfcom  9743  eldju1st  9966  coflim  10304  cflim2  10306  fin23lem11  10360  fin23lem26  10368  fin1a2lem13  10455  fpwwe2lem11  10684  suplem2pr  11096  axpre-sup  11212  axsup  11339  dedekind  11427  dedekindle  11428  fimaxre  12210  fiminre  12213  lbinf  12219  dfinfre  12247  infrelb  12251  suprfinzcl  12728  uzwo  12947  supminf  12971  lbzbi  12972  zsupss  12973  suprzcl2  12974  xrsupsslem  13340  xrinfmsslem  13341  xrub  13345  supxr2  13347  supxrun  13349  supxrunb1  13352  supxrbnd1  13354  supxrbnd2  13355  supxrub  13357  supxrbnd  13361  infxrlb  13367  elfzom1elp1fzo  13753  ssfzo12  13779  fsuppmapnn0fiublem  14010  fsuppmapnn0fiub  14011  fsuppmapnn0fiub0  14013  seqsplit  14055  shftlem  15073  rpnnen2lem10  16225  rpnnen2lem11  16226  gcdcllem1  16499  mrcuni  17634  isacs1i  17670  mreacs  17671  lubss  18538  gsumwspan  18836  subgint  19144  cntziinsn  19331  cntzsubg  19333  pmtrdifellem4  19477  subrngint  20542  cntzsubrng  20549  subrgint  20579  cntzsubr  20590  sraassab  21865  mdetunilem9  22613  tgcl  22963  fctop  22998  cctop  23000  neips  23108  cmpsub  23395  1stcelcls  23456  ssref  23507  comppfsc  23527  txbasval  23601  fgss2  23869  filconn  23878  filuni  23880  filssufilg  23906  fmfnfmlem4  23952  trust  24225  elmopn2  24442  metrest  24524  dscopn  24573  metds0  24857  cncfmet  24920  negcncf  24933  negcncfOLD  24934  iscmet2  25313  ovolfioo  25487  ovolficc  25488  itg1mulc  25725  ply1term  26231  plyconst  26233  reeff1olem  26476  nosupno  27733  nosupbday  27735  nosupbnd1lem5  27742  noinfno  27748  noinfbday  27750  noetasuplem4  27766  usgruspgrb  29119  ocsh  31216  ocorth  31224  spansncvi  31585  pjss1coi  32096  sumdmdii  32348  unidifsnel  32461  dfcnv2  32593  xrge0infss  32664  measdivcst  34057  measdivcstALTV  34058  dya2iocuni  34117  bnj1190  34853  nummin  34928  opnrebl  36032  opnrebl2  36033  fness  36061  nlpineqsn  37115  fin2so  37308  matunitlindflem1  37317  poimirlem27  37348  poimir  37354  frinfm  37436  filbcmb  37441  nnubfi  37451  nninfnub  37452  sstotbnd3  37477  bndss  37487  exidreslem  37578  isidlc  37716  idlnegcl  37723  intidl  37730  unichnidl  37732  pmapglb2N  39470  elpaddn0  39499  paddasslem9  39527  paddasslem10  39528  pclfinN  39599  polval2N  39605  diaglbN  40754  dihord6apre  40955  unielss  42883  onmaxnelsup  42888  onsupmaxb  42904  onsupeqnmax  42912  gneispace  43801  snsslVD  44505  snssl  44506  sstrALT2VD  44510  sstrALT2  44511  suctrALTcf  44598  suctrALTcfVD  44599  ssnel  44642  uzwo4  44654  infxrunb2  44983  infxrbnd2  44984  supxrunb3  45014  unb2ltle  45030  infxrpnf  45061  supminfxr  45079  sge0iunmptlemfi  46034  caratheodorylem2  46148  ovnlerp  46183  ssfz12  46927  prssspr  47057  prsssprel  47060  lindslinindimp2lem4  47844  lindslinindsimp2  47846  lincresunit3lem2  47863  lincresunit3  47864