Theorem elinel1 4151

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 3915	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simplbi 497	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906

This theorem is referenced by:  elin1d  4154  nel1nelin  4157  inss1  4187  predel  6277  fvcofneq  7036  frrlem4  8229  frrlem12  8237  erdisj  8690  f1opwfi  9254  fival  9313  fi0  9321  dffi2  9324  elfiun  9331  epfrs  9638  r0weon  9920  fodomfi2  9968  ackbij1lem6  10132  ackbij1lem9  10135  ackbij1lem10  10136  ackbij1lem11  10137  fin23lem24  10230  fin23lem26  10233  isfin1-3  10294  canthp1lem2  10562  dedekindle  11295  uzdisj  13511  nn0disj  13558  lo1resb  15485  rlimresb  15486  o1resb  15487  ackbijnn  15749  prmreclem2  16843  isacs2  17574  acsfn  17580  isdrs2  18227  isacs3lem  18463  psssdm2  18502  resscntz  19260  rngcid  20566  ringcid  20595  rhmsubclem3  20618  mplind  22023  clsval2  22992  mreclatdemoBAD  23038  ordtrest  23144  fincmp  23335  discmp  23340  uncmp  23345  ptcnplem  23563  txkgen  23594  infil  23805  hauspwpwf1  23929  alexsubALTlem3  23991  alexsubALTlem4  23992  blbas  24372  blres  24373  xrge0tsms  24777  nmhmcn  25074  ncvsge0  25107  cphsscph  25205  mbfadd  25616  mbfsub  25617  i1fima2  25634  i1fd  25636  mbfmul  25681  bddmulibl  25794  limcun  25850  pilem2  26416  rlimcnp2  26930  xrlimcnp  26932  ppiprm  27115  chtprm  27117  prmorcht  27142  rplogsumlem2  27450  dchrisum0re  27478  uhgrspansubgrlem  29312  disjin  32610  xrge0tsmsd  33104  eulerpartgbij  34478  pibt2  37561  dfadjliftmap2  38571  dfblockliftmap2  38574  eqvreldisj  38810  mhpind  42779  fiinfi  43756  gneispace  44317  ismnushort  44484  elpwinss  45236  restuni3  45304  disjinfi  45378  inmap  45395  iocopn  45708  icoopn  45713  icomnfinre  45740  uzinico  45747  islpcn  45825  lptre2pt  45826  limcresiooub  45828  limcresioolb  45829  limsupmnflem  45906  limsupresxr  45952  liminfresxr  45953  liminfvalxr  45969  liminf0  45979  icccncfext  46073  stoweidlem39  46225  stoweidlem50  46236  stoweidlem57  46243  fourierdlem32  46325  fourierdlem33  46326  fourierdlem48  46340  fourierdlem49  46341  fourierdlem71  46363  sge0rnre  46550  sge00  46562  sge0tsms  46566  sge0cl  46567  sge0fsum  46573  sge0sup  46577  sge0less  46578  sge0gerp  46581  sge0resplit  46592  sge0split  46595  sge0iunmptlemre  46601  caragendifcl  46700  hoiqssbllem3  46810  hspmbllem2  46813  pimiooltgt  46896  pimdecfgtioc  46901  pimincfltioc  46902  pimdecfgtioo  46903  pimincfltioo  46904  sssmf  46924  smfaddlem1  46949  smfaddlem2  46950  smfadd  46951  mbfpsssmf  46969  smfmul  46981  smfdiv  46983  smfsuplem1  46997  smfliminflem  47016  nthrucw  47072  fmtno4prm  47763  rhmsubcALTVlem3  48471