Theorem elinel1 4125

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

Step	Hyp	Ref	Expression
1		elin 3899	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simplbi 497	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  elin1d  4128  inss1  4159  predel  6212  fvcofneq  6951  frrlem4  8076  frrlem12  8084  wfrlem4OLD  8114  erdisj  8508  f1opwfi  9053  fival  9101  fi0  9109  dffi2  9112  elfiun  9119  epfrs  9420  r0weon  9699  fodomfi2  9747  ackbij1lem6  9912  ackbij1lem9  9915  ackbij1lem10  9916  ackbij1lem11  9917  fin23lem24  10009  fin23lem26  10012  isfin1-3  10073  canthp1lem2  10340  dedekindle  11069  uzdisj  13258  nn0disj  13301  lo1resb  15201  rlimresb  15202  o1resb  15203  ackbijnn  15468  prmreclem2  16546  isacs2  17279  acsfn  17285  isdrs2  17939  isacs3lem  18175  psssdm2  18214  resscntz  18853  mplind  21188  clsval2  22109  mreclatdemoBAD  22155  ordtrest  22261  fincmp  22452  discmp  22457  uncmp  22462  ptcnplem  22680  txkgen  22711  infil  22922  hauspwpwf1  23046  alexsubALTlem3  23108  alexsubALTlem4  23109  blbas  23491  blres  23492  xrge0tsms  23903  nmhmcn  24189  ncvsge0  24222  cphsscph  24320  mbfadd  24730  mbfsub  24731  i1fima2  24748  i1fd  24750  mbfmul  24796  bddmulibl  24908  limcun  24964  pilem2  25516  rlimcnp2  26021  xrlimcnp  26023  ppiprm  26205  chtprm  26207  prmorcht  26232  rplogsumlem2  26538  dchrisum0re  26566  uhgrspansubgrlem  27560  disjin  30826  xrge0tsmsd  31219  eulerpartgbij  32239  pibt2  35515  eqvreldisj  36654  mhpind  40206  fiinfi  41069  gneispace  41633  ismnushort  41808  elpwinss  42486  restuni3  42556  nel1nelin  42584  disjinfi  42620  inmap  42638  iocopn  42948  icoopn  42953  icomnfinre  42980  uzinico  42988  islpcn  43070  lptre2pt  43071  limcresiooub  43073  limcresioolb  43074  limsupmnflem  43151  limsupresxr  43197  liminfresxr  43198  liminfvalxr  43214  liminf0  43224  icccncfext  43318  stoweidlem39  43470  stoweidlem50  43481  stoweidlem57  43488  fourierdlem32  43570  fourierdlem33  43571  fourierdlem48  43585  fourierdlem49  43586  fourierdlem71  43608  sge0rnre  43792  sge00  43804  sge0tsms  43808  sge0cl  43809  sge0fsum  43815  sge0sup  43819  sge0less  43820  sge0gerp  43823  sge0resplit  43834  sge0split  43837  sge0iunmptlemre  43843  caragendifcl  43942  hoiqssbllem3  44052  hspmbllem2  44055  pimiooltgt  44135  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  sssmf  44161  smfaddlem1  44185  smfaddlem2  44186  smfadd  44187  mbfpsssmf  44205  smfmul  44216  smfdiv  44218  smfsuplem1  44231  smfliminflem  44250  fmtno4prm  44915  rngcid  45425  ringcid  45471  rhmsubclem3  45534  rhmsubcALTVlem3  45552