Theorem ssel2 3925

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808  df-ss 3915

This theorem is referenced by:  tz7.7  6340  onfr  6353  onmindif  6408  ordunisssuc  6422  ssimaex  6916  nssdmovg  7537  onnmin  7740  onmindif2  7749  limsssuc  7789  el2xpss  7978  1st2nd  7980  f1o2ndf1  8061  dfrecs3  8301  boxriin  8874  ordunifi  9185  isfinite2  9193  ordtypelem7  9421  sucprcreg  9501  cnfcom  9601  eldju1st  9827  coflim  10163  cflim2  10165  fin23lem11  10219  fin23lem26  10227  fin1a2lem13  10314  fpwwe2lem11  10543  suplem2pr  10955  axpre-sup  11071  axsup  11199  dedekind  11287  dedekindle  11288  fimaxre  12077  fiminre  12080  lbinf  12086  dfinfre  12114  infrelb  12118  suprfinzcl  12597  uzwo  12815  supminf  12839  lbzbi  12840  zsupss  12841  suprzcl2  12842  xrsupsslem  13213  xrinfmsslem  13214  xrub  13218  supxr2  13220  supxrun  13222  supxrunb1  13225  supxrbnd1  13227  supxrbnd2  13228  supxrub  13230  supxrbnd  13234  infxrlb  13241  elfzom1elp1fzo  13639  ssfzo12  13666  fsuppmapnn0fiublem  13904  fsuppmapnn0fiub  13905  fsuppmapnn0fiub0  13907  seqsplit  13949  shftlem  14982  rpnnen2lem10  16139  rpnnen2lem11  16140  gcdcllem1  16417  mrcuni  17535  isacs1i  17571  mreacs  17572  lubss  18427  gsumwspan  18762  subgint  19071  cntziinsn  19257  cntzsubg  19259  pmtrdifellem4  19399  subrngint  20484  cntzsubrng  20491  subrgint  20519  cntzsubr  20530  sraassab  21814  mdetunilem9  22555  tgcl  22904  fctop  22939  cctop  22941  neips  23048  cmpsub  23335  1stcelcls  23396  ssref  23447  comppfsc  23467  txbasval  23541  fgss2  23809  filconn  23818  filuni  23820  filssufilg  23846  fmfnfmlem4  23892  trust  24164  elmopn2  24380  metrest  24459  dscopn  24508  metds0  24786  cncfmet  24849  negcncf  24862  negcncfOLD  24863  iscmet2  25241  ovolfioo  25415  ovolficc  25416  itg1mulc  25652  ply1term  26156  plyconst  26158  reeff1olem  26403  nosupno  27662  nosupbday  27664  nosupbnd1lem5  27671  noinfno  27677  noinfbday  27679  noetasuplem4  27695  n0sfincut  28302  usgruspgrb  29182  ocsh  31284  ocorth  31292  spansncvi  31653  pjss1coi  32164  sumdmdii  32416  unidifsnel  32536  dfcnv2  32680  xrge0infss  32768  measdivcst  34309  measdivcstALTV  34310  dya2iocuni  34368  bnj1190  35092  nummin  35176  trssfir1om  35194  trssfir1omregs  35204  opnrebl  36436  opnrebl2  36437  fness  36465  nlpineqsn  37525  fin2so  37720  matunitlindflem1  37729  poimirlem27  37760  poimir  37766  frinfm  37848  filbcmb  37853  nnubfi  37863  nninfnub  37864  sstotbnd3  37889  bndss  37899  exidreslem  37990  isidlc  38128  idlnegcl  38135  intidl  38142  unichnidl  38144  pmapglb2N  39943  elpaddn0  39972  paddasslem9  40000  paddasslem10  40001  pclfinN  40072  polval2N  40078  diaglbN  41227  dihord6apre  41428  unielss  43375  onmaxnelsup  43380  onsupmaxb  43396  onsupeqnmax  43404  gneispace  44291  snsslVD  44985  snssl  44986  sstrALT2VD  44990  sstrALT2  44991  suctrALTcf  45078  suctrALTcfVD  45079  ssnel  45204  uzwo4  45214  infxrunb2  45528  infxrbnd2  45529  supxrunb3  45559  unb2ltle  45575  infxrpnf  45606  supminfxr  45624  sge0iunmptlemfi  46573  caratheodorylem2  46687  ovnlerp  46722  ssfz12  47476  prssspr  47647  prsssprel  47650  lindslinindimp2lem4  48623  lindslinindsimp2  48625  lincresunit3lem2  48642  lincresunit3  48643