Theorem ssel2 3930

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

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

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 3920

This theorem is referenced by:  tz7.7  6351  onfr  6364  onmindif  6419  ordunisssuc  6433  ssimaex  6927  nssdmovg  7550  onnmin  7753  onmindif2  7762  limsssuc  7802  el2xpss  7991  1st2nd  7993  f1o2ndf1  8074  dfrecs3  8314  boxriin  8890  ordunifi  9202  isfinite2  9210  ordtypelem7  9441  sucprcreg  9521  cnfcom  9621  eldju1st  9847  coflim  10183  cflim2  10185  fin23lem11  10239  fin23lem26  10247  fin1a2lem13  10334  fpwwe2lem11  10564  suplem2pr  10976  axpre-sup  11092  axsup  11220  dedekind  11308  dedekindle  11309  fimaxre  12098  fiminre  12101  lbinf  12107  dfinfre  12135  infrelb  12139  suprfinzcl  12618  uzwo  12836  supminf  12860  lbzbi  12861  zsupss  12862  suprzcl2  12863  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  supxr2  13241  supxrun  13243  supxrunb1  13246  supxrbnd1  13248  supxrbnd2  13249  supxrub  13251  supxrbnd  13255  infxrlb  13262  elfzom1elp1fzo  13660  ssfzo12  13687  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  fsuppmapnn0fiub0  13928  seqsplit  13970  shftlem  15003  rpnnen2lem10  16160  rpnnen2lem11  16161  gcdcllem1  16438  mrcuni  17556  isacs1i  17592  mreacs  17593  lubss  18448  gsumwspan  18783  subgint  19092  cntziinsn  19278  cntzsubg  19280  pmtrdifellem4  19420  subrngint  20505  cntzsubrng  20512  subrgint  20540  cntzsubr  20551  sraassab  21835  mdetunilem9  22576  tgcl  22925  fctop  22960  cctop  22962  neips  23069  cmpsub  23356  1stcelcls  23417  ssref  23468  comppfsc  23488  txbasval  23562  fgss2  23830  filconn  23839  filuni  23841  filssufilg  23867  fmfnfmlem4  23913  trust  24185  elmopn2  24401  metrest  24480  dscopn  24529  metds0  24807  cncfmet  24870  negcncf  24883  negcncfOLD  24884  iscmet2  25262  ovolfioo  25436  ovolficc  25437  itg1mulc  25673  ply1term  26177  plyconst  26179  reeff1olem  26424  nosupno  27683  nosupbday  27685  nosupbnd1lem5  27692  noinfno  27698  noinfbday  27700  noetasuplem4  27716  n0fincut  28363  usgruspgrb  29268  ocsh  31370  ocorth  31378  spansncvi  31739  pjss1coi  32250  sumdmdii  32502  unidifsnel  32621  dfcnv2  32764  xrge0infss  32850  measdivcst  34401  measdivcstALTV  34402  dya2iocuni  34460  bnj1190  35183  nummin  35268  trssfir1om  35286  trssfir1omregs  35311  opnrebl  36533  opnrebl2  36534  fness  36562  nlpineqsn  37660  fin2so  37855  matunitlindflem1  37864  poimirlem27  37895  poimir  37901  frinfm  37983  filbcmb  37988  nnubfi  37998  nninfnub  37999  sstotbnd3  38024  bndss  38034  exidreslem  38125  isidlc  38263  idlnegcl  38270  intidl  38277  unichnidl  38279  pmapglb2N  40144  elpaddn0  40173  paddasslem9  40201  paddasslem10  40202  pclfinN  40273  polval2N  40279  diaglbN  41428  dihord6apre  41629  unielss  43572  onmaxnelsup  43577  onsupmaxb  43593  onsupeqnmax  43601  gneispace  44487  snsslVD  45181  snssl  45182  sstrALT2VD  45186  sstrALT2  45187  suctrALTcf  45274  suctrALTcfVD  45275  ssnel  45400  uzwo4  45410  infxrunb2  45723  infxrbnd2  45724  supxrunb3  45754  unb2ltle  45770  infxrpnf  45801  supminfxr  45819  sge0iunmptlemfi  46768  caratheodorylem2  46882  ovnlerp  46917  ssfz12  47671  prssspr  47842  prsssprel  47845  lindslinindimp2lem4  48818  lindslinindsimp2  48820  lincresunit3lem2  48837  lincresunit3  48838