Theorem ssel2 3990

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106   ⊆ wss 3963

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 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814  df-ss 3980

This theorem is referenced by:  tz7.7  6412  onfr  6425  onmindif  6478  ordunisssuc  6492  ssimaex  6994  nssdmovg  7615  onnmin  7818  onmindif2  7827  limsssuc  7871  el2xpss  8061  1st2nd  8063  f1o2ndf1  8146  dfrecs3  8411  dfrecs3OLD  8412  boxriin  8979  ordunifi  9324  isfinite2  9332  ordtypelem7  9562  sucprcreg  9639  cnfcom  9738  eldju1st  9961  coflim  10299  cflim2  10301  fin23lem11  10355  fin23lem26  10363  fin1a2lem13  10450  fpwwe2lem11  10679  suplem2pr  11091  axpre-sup  11207  axsup  11334  dedekind  11422  dedekindle  11423  fimaxre  12210  fiminre  12213  lbinf  12219  dfinfre  12247  infrelb  12251  suprfinzcl  12730  uzwo  12951  supminf  12975  lbzbi  12976  zsupss  12977  suprzcl2  12978  xrsupsslem  13346  xrinfmsslem  13347  xrub  13351  supxr2  13353  supxrun  13355  supxrunb1  13358  supxrbnd1  13360  supxrbnd2  13361  supxrub  13363  supxrbnd  13367  infxrlb  13373  elfzom1elp1fzo  13768  ssfzo12  13795  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  fsuppmapnn0fiub0  14031  seqsplit  14073  shftlem  15104  rpnnen2lem10  16256  rpnnen2lem11  16257  gcdcllem1  16533  mrcuni  17666  isacs1i  17702  mreacs  17703  lubss  18571  gsumwspan  18872  subgint  19181  cntziinsn  19368  cntzsubg  19370  pmtrdifellem4  19512  subrngint  20577  cntzsubrng  20584  subrgint  20612  cntzsubr  20623  sraassab  21906  mdetunilem9  22642  tgcl  22992  fctop  23027  cctop  23029  neips  23137  cmpsub  23424  1stcelcls  23485  ssref  23536  comppfsc  23556  txbasval  23630  fgss2  23898  filconn  23907  filuni  23909  filssufilg  23935  fmfnfmlem4  23981  trust  24254  elmopn2  24471  metrest  24553  dscopn  24602  metds0  24886  cncfmet  24949  negcncf  24962  negcncfOLD  24963  iscmet2  25342  ovolfioo  25516  ovolficc  25517  itg1mulc  25754  ply1term  26258  plyconst  26260  reeff1olem  26505  nosupno  27763  nosupbday  27765  nosupbnd1lem5  27772  noinfno  27778  noinfbday  27780  noetasuplem4  27796  usgruspgrb  29215  ocsh  31312  ocorth  31320  spansncvi  31681  pjss1coi  32192  sumdmdii  32444  unidifsnel  32561  dfcnv2  32693  xrge0infss  32771  measdivcst  34205  measdivcstALTV  34206  dya2iocuni  34265  bnj1190  35001  nummin  35084  opnrebl  36303  opnrebl2  36304  fness  36332  nlpineqsn  37391  fin2so  37594  matunitlindflem1  37603  poimirlem27  37634  poimir  37640  frinfm  37722  filbcmb  37727  nnubfi  37737  nninfnub  37738  sstotbnd3  37763  bndss  37773  exidreslem  37864  isidlc  38002  idlnegcl  38009  intidl  38016  unichnidl  38018  pmapglb2N  39754  elpaddn0  39783  paddasslem9  39811  paddasslem10  39812  pclfinN  39883  polval2N  39889  diaglbN  41038  dihord6apre  41239  unielss  43207  onmaxnelsup  43212  onsupmaxb  43228  onsupeqnmax  43236  gneispace  44124  snsslVD  44827  snssl  44828  sstrALT2VD  44832  sstrALT2  44833  suctrALTcf  44920  suctrALTcfVD  44921  ssnel  44981  uzwo4  44993  infxrunb2  45318  infxrbnd2  45319  supxrunb3  45349  unb2ltle  45365  infxrpnf  45396  supminfxr  45414  sge0iunmptlemfi  46369  caratheodorylem2  46483  ovnlerp  46518  ssfz12  47264  prssspr  47410  prsssprel  47413  lindslinindimp2lem4  48307  lindslinindsimp2  48309  lincresunit3lem2  48326  lincresunit3  48327