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

Theorem elinel1 3943
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 3940 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21simplbi 478 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2140  cin 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-in 3723
This theorem is referenced by:  elin1d  3946  inss1  3977  predel  5859  prmreclem2  15844  txkgen  21678  ncvsge0  23174  pilem2  24426  dchrisum0re  25423  uhgrspansubgrlem  26403  disjin  29728  xrge0tsmsd  30116  eulerpartgbij  30765  frrlem4  32111  fiinfi  38399  gneispace  38953  elpwinss  39734  restuni3  39819  nel1nelin  39855  disjinfi  39898  inmap  39919  iocopn  40268  icoopn  40273  icomnfinre  40301  uzinico  40309  islpcn  40393  lptre2pt  40394  limcresiooub  40396  limcresioolb  40397  limsupmnflem  40474  limsupresxr  40520  liminfresxr  40521  liminfvalxr  40537  liminf0  40547  icccncfext  40622  stoweidlem39  40778  stoweidlem50  40789  stoweidlem57  40796  fourierdlem32  40878  fourierdlem33  40879  fourierdlem48  40893  fourierdlem49  40894  fourierdlem71  40916  sge0rnre  41103  sge00  41115  sge0tsms  41119  sge0cl  41120  sge0fsum  41126  sge0sup  41130  sge0less  41131  sge0gerp  41134  sge0resplit  41145  sge0split  41148  sge0iunmptlemre  41154  caragendifcl  41253  hoiqssbllem3  41363  hspmbllem2  41366  pimiooltgt  41446  pimdecfgtioc  41450  pimincfltioc  41451  pimdecfgtioo  41452  pimincfltioo  41453  sssmf  41472  smfaddlem1  41496  smfaddlem2  41497  smfadd  41498  mbfpsssmf  41516  smfmul  41527  smfdiv  41529  smfsuplem1  41542  smfliminflem  41561  fmtno4prm  42016  rngcid  42508  ringcid  42554  rhmsubclem3  42617  rhmsubcALTVlem3  42635
  Copyright terms: Public domain W3C validator