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

Theorem elinel1 3950
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 3947 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21simplbi 485 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  cin 3722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730
This theorem is referenced by:  elin1d  3953  inss1  3981  predel  5839  wfrlem4  7573  prmreclem2  15827  txkgen  21675  ncvsge0  23171  pilem2  24425  dchrisum0re  25422  uhgrspansubgrlem  26404  disjin  29736  xrge0tsmsd  30124  eulerpartgbij  30773  frrlem4  32119  fiinfi  38404  gneispace  38958  elpwinss  39737  restuni3  39822  nel1nelin  39856  disjinfi  39899  inmap  39918  iocopn  40262  icoopn  40267  icomnfinre  40294  uzinico  40302  islpcn  40386  lptre2pt  40387  limcresiooub  40389  limcresioolb  40390  limsupmnflem  40467  limsupresxr  40513  liminfresxr  40514  liminfvalxr  40530  liminf0  40540  icccncfext  40615  stoweidlem39  40770  stoweidlem50  40781  stoweidlem57  40788  fourierdlem32  40870  fourierdlem33  40871  fourierdlem48  40885  fourierdlem49  40886  fourierdlem71  40908  sge0rnre  41095  sge00  41107  sge0tsms  41111  sge0cl  41112  sge0fsum  41118  sge0sup  41122  sge0less  41123  sge0gerp  41126  sge0resplit  41137  sge0split  41140  sge0iunmptlemre  41146  caragendifcl  41245  hoiqssbllem3  41355  hspmbllem2  41358  pimiooltgt  41438  pimdecfgtioc  41442  pimincfltioc  41443  pimdecfgtioo  41444  pimincfltioo  41445  sssmf  41464  smfaddlem1  41488  smfaddlem2  41489  smfadd  41490  mbfpsssmf  41508  smfmul  41519  smfdiv  41521  smfsuplem1  41534  smfliminflem  41553  fmtno4prm  42012  rngcid  42504  ringcid  42550  rhmsubclem3  42613  rhmsubcALTVlem3  42631
  Copyright terms: Public domain W3C validator