Theorem ssel2 3933

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3923

This theorem is referenced by:  tz7.7  6388  onfr  6402  onmindif  6457  ordunisssuc  6471  ssimaex  6968  nssdmovg  7594  onnmin  7798  onmindif2  7807  limsssuc  7847  el2xpss  8035  1st2nd  8037  f1o2ndf1  8118  dfrecs3  8360  boxriin  8939  ordunifi  9251  isfinite2  9259  ordtypelem7  9487  sucprcregOLD  9570  cnfcom  9670  eldju1st  9910  coflim  10246  cflim2  10248  fin23lem11  10302  fin23lem26  10310  fin1a2lem13  10397  fpwwe2lem11  10627  suplem2pr  11039  axpre-sup  11155  axsup  11286  dedekind  11374  dedekindle  11375  fimaxre  12160  fiminre  12163  lbinf  12169  dfinfre  12197  infrelb  12201  suprfinzcl  12711  uzwo  12936  supminf  12960  lbzbi  12961  zsupss  12962  suprzcl2  12963  xrsupsslem  13334  xrinfmsslem  13335  xrub  13339  supxr2  13341  supxrun  13343  supxrunb1  13346  supxrbnd1  13348  supxrbnd2  13349  supxrub  13351  supxrbnd  13355  infxrlb  13362  elfzom1elp1fzo  13763  ssfzo12  13790  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  fsuppmapnn0fiub0  14031  seqsplit  14073  shftlem  15107  rpnnen2lem10  16280  rpnnen2lem11  16281  gcdcllem1  16558  mrcuni  17678  isacs1i  17714  mreacs  17715  lubss  18570  gsumwspan  18906  subgint  19218  cntziinsn  19408  cntzsubg  19410  pmtrdifellem4  19550  subrngint  20646  cntzsubrng  20653  subrgint  20681  cntzsubr  20692  sraassab  21999  mdetunilem9  22758  tgcl  23107  fctop  23142  cctop  23144  neips  23251  cmpsub  23538  1stcelcls  23599  ssref  23650  comppfsc  23670  txbasval  23744  fgss2  24012  filconn  24021  filuni  24023  filssufilg  24049  fmfnfmlem4  24095  trust  24367  elmopn2  24583  metrest  24662  dscopn  24711  metds0  24989  cncfmet  25049  negcncf  25062  iscmet2  25434  ovolfioo  25607  ovolficc  25608  itg1mulc  25844  ply1term  26342  plyconst  26344  reeff1olem  26590  nosupno  27848  nosupbday  27850  nosupbnd1lem5  27857  noinfno  27863  noinfbday  27865  noetasuplem4  27881  n0fincut  28529  usgruspgrb  29514  ocsh  31616  ocorth  31624  spansncvi  31985  pjss1coi  32496  sumdmdii  32748  unidifsnel  32862  dfcnv2  33001  xrge0infss  33086  measdivcst  34595  measdivcstALTV  34596  dya2iocuni  34654  bnj1190  35377  nummin  35465  trssfir1om  35488  trssfir1omregs  35530  opnrebl  36812  opnrebl2  36813  fness  36841  ttcmin  36988  nlpineqsn  38035  fin2so  38239  matunitlindflem1  38248  poimirlem27  38279  poimir  38285  frinfm  38367  filbcmb  38372  nnubfi  38382  nninfnub  38383  sstotbnd3  38408  bndss  38418  exidreslem  38509  isidlc  38647  idlnegcl  38654  intidl  38661  unichnidl  38663  pmapglb2N  40526  elpaddn0  40555  paddasslem9  40583  paddasslem10  40584  pclfinN  40655  polval2N  40661  diaglbN  41810  dihord6apre  42011  unielss  43928  onmaxnelsup  43933  onsupmaxb  43949  onsupeqnmax  43957  gneispace  44843  snsslVD  45520  snssl  45521  sstrALT2VD  45525  sstrALT2  45526  suctrALTcf  45613  suctrALTcfVD  45614  ssnel  45746  uzwo4  45756  infxrunb2  46066  infxrbnd2  46067  supxrunb3  46097  unb2ltle  46112  infxrpnf  46143  supminfxr  46161  sge0iunmptlemfi  47110  caratheodorylem2  47224  ovnlerp  47259  ssfz12  48034  prssspr  48217  prsssprel  48220  lindslinindimp2lem4  49224  lindslinindsimp2  49226  lincresunit3lem2  49243  lincresunit3  49244