Theorem ssel2 3882

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  tz7.7  6217  onfr  6230  onmindif  6280  ordunisssuc  6293  ssimaex  6774  nssdmovg  7368  onnmin  7560  onmindif2  7569  limsssuc  7607  1st2nd  7788  f1o2ndf1  7869  dfrecs3  8087  boxriin  8599  ordunifi  8899  isfinite2  8907  ordtypelem7  9118  sucprcreg  9195  cnfcom  9293  eldju1st  9504  coflim  9840  cflim2  9842  fin23lem11  9896  fin23lem26  9904  fin1a2lem13  9991  fpwwe2lem11  10220  suplem2pr  10632  axpre-sup  10748  axsup  10873  dedekind  10960  dedekindle  10961  fimaxre  11741  fiminre  11744  lbinf  11750  dfinfre  11778  infrelb  11782  suprfinzcl  12257  uzwo  12472  supminf  12496  lbzbi  12497  zsupss  12498  suprzcl2  12499  xrsupsslem  12862  xrinfmsslem  12863  xrub  12867  supxr2  12869  supxrun  12871  supxrunb1  12874  supxrbnd1  12876  supxrbnd2  12877  supxrub  12879  supxrbnd  12883  infxrlb  12889  elfzom1elp1fzo  13274  ssfzo12  13300  fsuppmapnn0fiublem  13528  fsuppmapnn0fiub  13529  fsuppmapnn0fiub0  13531  seqsplit  13574  shftlem  14596  rpnnen2lem10  15747  rpnnen2lem11  15748  gcdcllem1  16021  mrcuni  17078  isacs1i  17114  mreacs  17115  lubss  17973  gsumwspan  18227  subgint  18521  cntziinsn  18683  cntzsubg  18685  pmtrdifellem4  18825  subrgint  19776  cntzsubr  19787  mdetunilem9  21471  tgcl  21820  fctop  21855  cctop  21857  neips  21964  cmpsub  22251  1stcelcls  22312  ssref  22363  comppfsc  22383  txbasval  22457  fgss2  22725  filconn  22734  filuni  22736  filssufilg  22762  fmfnfmlem4  22808  trust  23081  elmopn2  23297  metrest  23376  dscopn  23425  metds0  23701  cncfmet  23760  negcncf  23773  iscmet2  24145  ovolfioo  24318  ovolficc  24319  itg1mulc  24556  ply1term  25052  plyconst  25054  reeff1olem  25292  usgruspgrb  27226  ocsh  29318  ocorth  29326  spansncvi  29687  pjss1coi  30198  sumdmdii  30450  unidifsnel  30556  dfcnv2  30687  xrge0infss  30757  measdivcst  31858  measdivcstALTV  31859  dya2iocuni  31916  bnj1190  32655  nummin  32730  elxpxpss  33354  nosupno  33592  nosupbday  33594  nosupbnd1lem5  33601  noinfno  33607  noinfbday  33609  noetasuplem4  33625  opnrebl  34195  opnrebl2  34196  fness  34224  nlpineqsn  35265  fin2so  35450  matunitlindflem1  35459  poimirlem27  35490  poimir  35496  frinfm  35579  filbcmb  35584  nnubfi  35594  nninfnub  35595  sstotbnd3  35620  bndss  35630  exidreslem  35721  isidlc  35859  idlnegcl  35866  intidl  35873  unichnidl  35875  pmapglb2N  37471  elpaddn0  37500  paddasslem9  37528  paddasslem10  37529  pclfinN  37600  polval2N  37606  diaglbN  38755  dihord6apre  38956  gneispace  41362  snsslVD  42063  snssl  42064  sstrALT2VD  42068  sstrALT2  42069  suctrALTcf  42156  suctrALTcfVD  42157  ssnel  42202  uzwo4  42215  infxrunb2  42521  infxrbnd2  42522  supxrunb3  42553  unb2ltle  42569  infxrpnf  42601  supminfxr  42620  sge0iunmptlemfi  43569  caratheodorylem2  43683  ovnlerp  43718  ssfz12  44422  prssspr  44553  prsssprel  44556  lindslinindimp2lem4  45418  lindslinindsimp2  45420  lincresunit3lem2  45437  lincresunit3  45438