Theorem ssel2 3962

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  tz7.7  6217  onfr  6230  onmindif  6280  ordunisssuc  6293  ssimaex  6748  nssdmovg  7330  onnmin  7518  onmindif2  7527  limsssuc  7565  1st2nd  7738  f1o2ndf1  7818  dfrecs3  8009  boxriin  8504  ordunifi  8768  isfinite2  8776  ordtypelem7  8988  sucprcreg  9065  cnfcom  9163  eldju1st  9352  coflim  9683  cflim2  9685  fin23lem11  9739  fin23lem26  9747  fin1a2lem13  9834  fpwwe2lem12  10063  suplem2pr  10475  axpre-sup  10591  axsup  10716  dedekind  10803  dedekindle  10804  fimaxre  11584  fiminre  11588  lbinf  11594  dfinfre  11622  infrelb  11626  suprfinzcl  12098  uzwo  12312  supminf  12336  lbzbi  12337  zsupss  12338  suprzcl2  12339  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  supxr2  12708  supxrun  12710  supxrunb1  12713  supxrbnd1  12715  supxrbnd2  12716  supxrub  12718  supxrbnd  12722  infxrlb  12728  elfzom1elp1fzo  13105  ssfzo12  13131  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  fsuppmapnn0fiub0  13362  seqsplit  13404  shftlem  14427  rpnnen2lem10  15576  rpnnen2lem11  15577  gcdcllem1  15848  mrcuni  16892  isacs1i  16928  mreacs  16929  lubss  17731  gsumwspan  18011  subgint  18303  cntziinsn  18465  cntzsubg  18467  pmtrdifellem4  18607  subrgint  19557  cntzsubr  19568  mdetunilem9  21229  tgcl  21577  fctop  21612  cctop  21614  neips  21721  cmpsub  22008  1stcelcls  22069  ssref  22120  comppfsc  22140  txbasval  22214  fgss2  22482  filconn  22491  filuni  22493  filssufilg  22519  fmfnfmlem4  22565  trust  22838  elmopn2  23055  metrest  23134  dscopn  23183  metds0  23458  cncfmet  23516  negcncf  23526  iscmet2  23897  ovolfioo  24068  ovolficc  24069  itg1mulc  24305  ply1term  24794  plyconst  24796  reeff1olem  25034  usgruspgrb  26966  ocsh  29060  ocorth  29068  spansncvi  29429  pjss1coi  29940  sumdmdii  30192  unidifsnel  30295  dfcnv2  30422  xrge0infss  30484  measdivcst  31483  measdivcstALTV  31484  dya2iocuni  31541  bnj1190  32280  nosupno  33203  nosupbday  33205  nosupbnd1lem5  33212  noetalem3  33219  opnrebl  33668  opnrebl2  33669  fness  33697  nlpineqsn  34692  fin2so  34894  matunitlindflem1  34903  poimirlem27  34934  poimir  34940  frinfm  35025  filbcmb  35030  nnubfi  35040  nninfnub  35041  sstotbnd3  35069  bndss  35079  exidreslem  35170  isidlc  35308  idlnegcl  35315  intidl  35322  unichnidl  35324  pmapglb2N  36922  elpaddn0  36951  paddasslem9  36979  paddasslem10  36980  pclfinN  37051  polval2N  37057  diaglbN  38206  dihord6apre  38407  gneispace  40504  snsslVD  41183  snssl  41184  sstrALT2VD  41188  sstrALT2  41189  suctrALTcf  41276  suctrALTcfVD  41277  ssnel  41322  uzwo4  41335  infxrunb2  41656  infxrbnd2  41657  supxrunb3  41692  unb2ltle  41709  infxrpnf  41741  supminfxr  41760  sge0iunmptlemfi  42715  caratheodorylem2  42829  ovnlerp  42864  ssfz12  43534  prssspr  43667  prsssprel  43670  lindslinindimp2lem4  44536  lindslinindsimp2  44538  lincresunit3lem2  44555  lincresunit3  44556