Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elinel1 Structured version   Visualization version   GIF version

Theorem elinel1 3782
 Description: Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
elinel1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)

Proof of Theorem elinel1
StepHypRef Expression
1 elin 3779 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21simplbi 476 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1987   ∩ cin 3558 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-in 3566 This theorem is referenced by:  elin1d  3785  inss1  3816  predel  5661  prmreclem2  15556  txkgen  21378  ncvsge0  22876  dchrisum0re  25119  uhgrspansubgrlem  26092  disjin  29267  xrge0tsmsd  29594  eulerpartgbij  30239  fiinfi  37394  gneispace  37949  elpwinss  38734  restuni3  38822  disjinfi  38885  inmap  38906  iocopn  39188  icoopn  39193  icomnfinre  39221  uzinico  39229  islpcn  39303  lptre2pt  39304  limcresiooub  39306  limcresioolb  39307  limsupmnflem  39384  icccncfext  39431  stoweidlem39  39589  stoweidlem50  39600  stoweidlem57  39607  fourierdlem32  39689  fourierdlem33  39690  fourierdlem48  39704  fourierdlem49  39705  fourierdlem71  39727  sge0rnre  39914  sge00  39926  sge0tsms  39930  sge0cl  39931  sge0fsum  39937  sge0sup  39941  sge0less  39942  sge0gerp  39945  sge0resplit  39956  sge0split  39959  sge0iunmptlemre  39965  caragendifcl  40061  hoiqssbllem3  40171  hspmbllem2  40174  pimiooltgt  40254  pimdecfgtioc  40258  pimincfltioc  40259  pimdecfgtioo  40260  pimincfltioo  40261  sssmf  40280  smfaddlem1  40304  smfaddlem2  40305  smfadd  40306  mbfpsssmf  40324  smfmul  40335  smfdiv  40337  smfsuplem1  40350  fmtno4prm  40812  rngcid  41293  ringcid  41339  rhmsubclem3  41402  rhmsubcALTVlem3  41420
 Copyright terms: Public domain W3C validator