Theorem ssel2 3852

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048   ⊆ wss 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-in 3835  df-ss 3842

This theorem is referenced by:  tz7.7  6053  onfr  6066  onmindif  6116  ordunisssuc  6129  ssimaex  6574  nssdmovg  7144  onnmin  7332  onmindif2  7341  limsssuc  7379  1st2nd  7547  f1o2ndf1  7620  dfrecs3  7810  boxriin  8297  ordunifi  8559  isfinite2  8567  ordtypelem7  8779  sucprcreg  8856  cnfcom  8953  eldju1st  9142  coflim  9477  cflim2  9479  fin23lem11  9533  fin23lem26  9541  fin1a2lem13  9628  fpwwe2lem12  9857  suplem2pr  10269  axpre-sup  10385  axsup  10512  dedekind  10599  dedekindle  10600  fimaxre  11381  fiminre  11385  lbinf  11391  dfinfre  11419  infrelb  11423  suprfinzcl  11907  uzwo  12122  supminf  12146  lbzbi  12147  zsupss  12148  suprzcl2  12149  xrsupsslem  12513  xrinfmsslem  12514  xrub  12518  supxr2  12520  supxrun  12522  supxrunb1  12525  supxrbnd1  12527  supxrbnd2  12528  supxrub  12530  supxrbnd  12534  infxrlb  12540  elfzom1elp1fzo  12916  ssfzo12  12942  fsuppmapnn0fiublem  13170  fsuppmapnn0fiub  13171  fsuppmapnn0fiub0  13173  seqsplit  13215  shftlem  14282  rpnnen2lem10  15430  rpnnen2lem11  15431  gcdcllem1  15702  mrcuni  16744  isacs1i  16780  mreacs  16781  lubss  17583  gsumwspan  17846  subgint  18081  cntziinsn  18230  cntzsubg  18232  pmtrdifellem4  18362  subrgint  19274  cntzsubr  19284  mdetunilem9  20927  tgcl  21275  fctop  21310  cctop  21312  neips  21419  cmpsub  21706  1stcelcls  21767  ssref  21818  comppfsc  21838  txbasval  21912  fgss2  22180  filconn  22189  filuni  22191  filssufilg  22217  fmfnfmlem4  22263  trust  22535  elmopn2  22752  metrest  22831  dscopn  22880  metds0  23155  cncfmet  23213  negcncf  23223  iscmet2  23594  ovolfioo  23765  ovolficc  23766  itg1mulc  24002  ply1term  24491  plyconst  24493  reeff1olem  24731  usgruspgrb  26663  ocsh  28835  ocorth  28843  spansncvi  29204  pjss1coi  29715  sumdmdii  29967  dfcnv2  30178  xrge0infss  30230  measres  31117  measdivcstOLD  31119  measdivcst  31120  dya2iocuni  31177  bnj1190  31916  nosupno  32694  nosupbday  32696  nosupbnd1lem5  32703  noetalem3  32710  opnrebl  33159  opnrebl2  33160  fness  33188  nlpineqsn  34095  fin2so  34298  matunitlindflem1  34307  poimirlem27  34338  poimir  34344  frinfm  34430  filbcmb  34435  nnubfi  34445  nninfnub  34446  sstotbnd3  34474  bndss  34484  exidreslem  34575  isidlc  34713  idlnegcl  34720  intidl  34727  unichnidl  34729  pmapglb2N  36330  elpaddn0  36359  paddasslem9  36387  paddasslem10  36388  pclfinN  36459  polval2N  36465  diaglbN  37614  dihord6apre  37815  gneispace  39825  snsslVD  40559  snssl  40560  sstrALT2VD  40564  sstrALT2  40565  suctrALTcf  40652  suctrALTcfVD  40653  ssnel  40698  uzwo4  40712  infxrunb2  41044  infxrbnd2  41045  supxrunb3  41081  unb2ltle  41099  infxrpnf  41131  supminfxr  41150  sge0iunmptlemfi  42105  caratheodorylem2  42219  ovnlerp  42254  ssfz12  42899  prssspr  42989  prsssprel  42992  lindslinindimp2lem4  43857  lindslinindsimp2  43859  lincresunit3lem2  43876  lincresunit3  43877