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

Theorem elinel1 4156
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 3927 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21simplbi 499 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cin 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918
This theorem is referenced by:  elin1d  4159  inss1  4189  predel  6275  fvcofneq  7044  frrlem4  8221  frrlem12  8229  wfrlem4OLD  8259  erdisj  8703  f1opwfi  9303  fival  9353  fi0  9361  dffi2  9364  elfiun  9371  epfrs  9672  r0weon  9953  fodomfi2  10001  ackbij1lem6  10166  ackbij1lem9  10169  ackbij1lem10  10170  ackbij1lem11  10171  fin23lem24  10263  fin23lem26  10266  isfin1-3  10327  canthp1lem2  10594  dedekindle  11324  uzdisj  13520  nn0disj  13563  lo1resb  15452  rlimresb  15453  o1resb  15454  ackbijnn  15718  prmreclem2  16794  isacs2  17538  acsfn  17544  isdrs2  18200  isacs3lem  18436  psssdm2  18475  resscntz  19117  mplind  21494  clsval2  22417  mreclatdemoBAD  22463  ordtrest  22569  fincmp  22760  discmp  22765  uncmp  22770  ptcnplem  22988  txkgen  23019  infil  23230  hauspwpwf1  23354  alexsubALTlem3  23416  alexsubALTlem4  23417  blbas  23799  blres  23800  xrge0tsms  24213  nmhmcn  24499  ncvsge0  24533  cphsscph  24631  mbfadd  25041  mbfsub  25042  i1fima2  25059  i1fd  25061  mbfmul  25107  bddmulibl  25219  limcun  25275  pilem2  25827  rlimcnp2  26332  xrlimcnp  26334  ppiprm  26516  chtprm  26518  prmorcht  26543  rplogsumlem2  26849  dchrisum0re  26877  uhgrspansubgrlem  28280  disjin  31550  xrge0tsmsd  31948  eulerpartgbij  33029  pibt2  35934  eqvreldisj  37122  mhpind  40812  fiinfi  41933  gneispace  42494  ismnushort  42669  elpwinss  43345  restuni3  43416  nel1nelin  43444  disjinfi  43500  inmap  43517  iocopn  43844  icoopn  43849  icomnfinre  43876  uzinico  43884  islpcn  43966  lptre2pt  43967  limcresiooub  43969  limcresioolb  43970  limsupmnflem  44047  limsupresxr  44093  liminfresxr  44094  liminfvalxr  44110  liminf0  44120  icccncfext  44214  stoweidlem39  44366  stoweidlem50  44377  stoweidlem57  44384  fourierdlem32  44466  fourierdlem33  44467  fourierdlem48  44481  fourierdlem49  44482  fourierdlem71  44504  sge0rnre  44691  sge00  44703  sge0tsms  44707  sge0cl  44708  sge0fsum  44714  sge0sup  44718  sge0less  44719  sge0gerp  44722  sge0resplit  44733  sge0split  44736  sge0iunmptlemre  44742  caragendifcl  44841  hoiqssbllem3  44951  hspmbllem2  44954  pimiooltgt  45037  pimdecfgtioc  45042  pimincfltioc  45043  pimdecfgtioo  45044  pimincfltioo  45045  sssmf  45065  smfaddlem1  45090  smfaddlem2  45091  smfadd  45092  mbfpsssmf  45110  smfmul  45122  smfdiv  45124  smfsuplem1  45138  smfliminflem  45157  fmtno4prm  45853  rngcid  46363  ringcid  46409  rhmsubclem3  46472  rhmsubcALTVlem3  46490
  Copyright terms: Public domain W3C validator