Theorem ssel2 3961

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951

This theorem is referenced by:  tz7.7  6216  onfr  6229  onmindif  6279  ordunisssuc  6292  ssimaex  6747  nssdmovg  7329  onnmin  7517  onmindif2  7526  limsssuc  7564  1st2nd  7737  f1o2ndf1  7817  dfrecs3  8008  boxriin  8503  ordunifi  8767  isfinite2  8775  ordtypelem7  8987  sucprcreg  9064  cnfcom  9162  eldju1st  9351  coflim  9682  cflim2  9684  fin23lem11  9738  fin23lem26  9746  fin1a2lem13  9833  fpwwe2lem12  10062  suplem2pr  10474  axpre-sup  10590  axsup  10715  dedekind  10802  dedekindle  10803  fimaxre  11583  fiminre  11587  lbinf  11593  dfinfre  11621  infrelb  11625  suprfinzcl  12096  uzwo  12310  supminf  12334  lbzbi  12335  zsupss  12336  suprzcl2  12337  xrsupsslem  12699  xrinfmsslem  12700  xrub  12704  supxr2  12706  supxrun  12708  supxrunb1  12711  supxrbnd1  12713  supxrbnd2  12714  supxrub  12716  supxrbnd  12720  infxrlb  12726  elfzom1elp1fzo  13103  ssfzo12  13129  fsuppmapnn0fiublem  13357  fsuppmapnn0fiub  13358  fsuppmapnn0fiub0  13360  seqsplit  13402  shftlem  14426  rpnnen2lem10  15575  rpnnen2lem11  15576  gcdcllem1  15847  mrcuni  16891  isacs1i  16927  mreacs  16928  lubss  17730  gsumwspan  18010  subgint  18302  cntziinsn  18464  cntzsubg  18466  pmtrdifellem4  18606  subrgint  19556  cntzsubr  19567  mdetunilem9  21228  tgcl  21576  fctop  21611  cctop  21613  neips  21720  cmpsub  22007  1stcelcls  22068  ssref  22119  comppfsc  22139  txbasval  22213  fgss2  22481  filconn  22490  filuni  22492  filssufilg  22518  fmfnfmlem4  22564  trust  22837  elmopn2  23054  metrest  23133  dscopn  23182  metds0  23457  cncfmet  23515  negcncf  23525  iscmet2  23896  ovolfioo  24067  ovolficc  24068  itg1mulc  24304  ply1term  24793  plyconst  24795  reeff1olem  25033  usgruspgrb  26965  ocsh  29059  ocorth  29067  spansncvi  29428  pjss1coi  29939  sumdmdii  30191  unidifsnel  30294  dfcnv2  30421  xrge0infss  30483  measdivcst  31483  measdivcstALTV  31484  dya2iocuni  31541  bnj1190  32280  nosupno  33203  nosupbday  33205  nosupbnd1lem5  33212  noetalem3  33219  opnrebl  33668  opnrebl2  33669  fness  33697  nlpineqsn  34688  fin2so  34878  matunitlindflem1  34887  poimirlem27  34918  poimir  34924  frinfm  35009  filbcmb  35014  nnubfi  35024  nninfnub  35025  sstotbnd3  35053  bndss  35063  exidreslem  35154  isidlc  35292  idlnegcl  35299  intidl  35306  unichnidl  35308  pmapglb2N  36906  elpaddn0  36935  paddasslem9  36963  paddasslem10  36964  pclfinN  37035  polval2N  37041  diaglbN  38190  dihord6apre  38391  gneispace  40482  snsslVD  41161  snssl  41162  sstrALT2VD  41166  sstrALT2  41167  suctrALTcf  41254  suctrALTcfVD  41255  ssnel  41300  uzwo4  41313  infxrunb2  41634  infxrbnd2  41635  supxrunb3  41670  unb2ltle  41687  infxrpnf  41719  supminfxr  41738  sge0iunmptlemfi  42694  caratheodorylem2  42808  ovnlerp  42843  ssfz12  43513  prssspr  43646  prsssprel  43649  lindslinindimp2lem4  44515  lindslinindsimp2  44517  lincresunit3lem2  44534  lincresunit3  44535