Theorem ssel2 3563

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  tz7.7  5666  onfr  5680  onmindif  5732  ordunisssuc  5747  ssimaex  6173  nssdmovg  6714  onnmin  6895  onmindif2  6904  limsssuc  6942  1st2nd  7105  f1o2ndf1  7172  dfrecs3  7356  boxriin  7836  ordunifi  8095  isfinite2  8103  ordtypelem7  8312  sucprcreg  8389  cnfcom  8480  coflim  8966  cflim2  8968  fin23lem11  9022  fin23lem26  9030  fin1a2lem13  9117  fpwwe2lem12  9342  suplem2pr  9754  axpre-sup  9869  axsup  9992  dedekind  10079  dedekindle  10080  lbinf  10855  dfinfre  10881  infrelb  10885  suprfinzcl  11368  uzwo  11627  supminf  11651  lbzbi  11652  zsupss  11653  suprzcl2  11654  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  supxr2  12016  supxrun  12018  supxrunb1  12021  supxrbnd1  12023  supxrbnd2  12024  supxrub  12026  supxrbnd  12030  infxrlb  12036  elfzom1elp1fzo  12402  ssfzo12  12427  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  fsuppmapnn0fiub0  12655  seqsplit  12696  shftlem  13656  rpnnen2lem10  14791  rpnnen2lem11  14792  gcdcllem1  15059  mrcuni  16104  isacs1i  16141  mreacs  16142  lubss  16944  gsumwspan  17206  subgint  17441  cntziinsn  17590  cntzsubg  17592  pmtrdifellem4  17722  subrgint  18625  cntzsubr  18635  mdetunilem9  20245  tgcl  20584  fctop  20618  cctop  20620  neips  20727  cmpsub  21013  1stcelcls  21074  ssref  21125  comppfsc  21145  txbasval  21219  fgss2  21488  filcon  21497  filuni  21499  filssufilg  21525  fmfnfmlem4  21571  trust  21843  elmopn2  22060  metrest  22139  dscopn  22188  metds0  22461  cncfmet  22519  negcncf  22529  iscmet2  22900  ovolfioo  23043  ovolficc  23044  itg1mulc  23277  ply1term  23764  plyconst  23766  reeff1olem  24004  usgraedgrnv  25906  ocsh  27526  ocorth  27534  spansncvi  27895  pjss1coi  28406  sumdmdii  28658  dfcnv2  28859  xrge0infss  28915  measres  29612  measdivcstOLD  29614  measdivcst  29615  dya2iocuni  29672  bnj1190  30330  frrlem5e  31032  nobndlem2  31092  nobndlem6  31096  nobndlem8  31098  nobndup  31099  nobnddown  31100  nofulllem3  31103  nofulllem4  31104  nofulllem5  31105  opnrebl  31485  opnrebl2  31486  fness  31514  fin2so  32566  matunitlindflem1  32575  poimirlem27  32606  poimir  32612  frinfm  32700  filbcmb  32705  nnubfi  32716  nninfnub  32717  sstotbnd3  32745  bndss  32755  exidreslem  32846  isidlc  32984  idlnegcl  32991  intidl  32998  unichnidl  33000  pmapglb2N  34075  elpaddn0  34104  paddasslem9  34132  paddasslem10  34133  pclfinN  34204  polval2N  34210  diaglbN  35362  dihord6apre  35563  gneispace  37452  snsslVD  38086  snssl  38087  sstrALT2VD  38091  sstrALT2  38092  suctrALTcf  38180  suctrALTcfVD  38181  ssnel  38227  uzwo4  38246  infxrunb2  38525  infxrbnd2  38526  sge0iunmptlemfi  39306  caratheodorylem2  39417  ovnlerp  39452  ssfz12  40351  usgruspgrb  40411  lindslinindimp2lem4  42044  lindslinindsimp2  42046  lincresunit3lem2  42063  lincresunit3  42064