Theorem elinel1 4147

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 502	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906

This theorem is used by:  elin1d  4150  nel1nelin  4153  inss1  4182  predel  6324  fvcofneq  7093  frrlem4  8307  frrlem12  8315  erdisj  8775  f1opwfi  9345  fival  9404  fi0  9412  dffi2  9415  elfiun  9422  epfrs  9732  r0weon  10091  fodomfi2  10139  ackbij1lem6  10302  ackbij1lem9  10305  ackbij1lem10  10306  ackbij1lem11  10307  fin23lem24  10400  fin23lem26  10403  isfin1-3  10464  canthp1lem2  10738  dedekindle  11474  uzdisj  13731  nn0disj  13778  lo1resb  15731  rlimresb  15732  o1resb  15733  ackbijnn  15997  prmreclem2  17095  isacs2  17827  acsfn  17833  isdrs2  18480  isacs3lem  18716  psssdm2  18755  resscntz  19547  rngcid  20887  ringcid  20916  rhmsubclem3  20939  mplind  22379  clsval2  23368  mreclatdemoBAD  23414  ordtrest  23520  fincmp  23711  discmp  23716  uncmp  23721  ptcnplem  23940  txkgen  23971  infil  24182  hauspwpwf1  24306  alexsubALTlem3  24368  alexsubALTlem4  24369  blbas  24749  blres  24750  xrge0tsms  25154  nmhmcn  25441  ncvsge0  25474  cphsscph  25572  mbfadd  25982  mbfsub  25983  i1fima2  26000  i1fd  26002  mbfmul  26047  bddmulibl  26159  limcun  26215  pilem2  26779  rlimcnp2  27294  xrlimcnp  27296  ppiprm  27478  chtprm  27480  prmorcht  27505  rplogsumlem2  27812  dchrisum0re  27840  uhgrspansubgrlem  29871  disjin  33180  xrge0tsmsd  33634  eulerpartgbij  35004  dfttc4  37318  pibt2  38340  dfadjliftmap2  39389  dfblockliftmap2  39393  eqvreldisj  39630  mhpind  43622  fiinfi  44573  gneispace  45133  ismnushort  45284  hfstructstruct  46024  elpwinss  46065  restuni3  46132  disjinfi  46206  inmap  46221  iocopn  46531  icoopn  46536  icomnfinre  46563  uzinico  46570  islpcn  46648  lptre2pt  46649  limcresiooub  46651  limcresioolb  46652  limsupmnflem  46729  limsupresxr  46775  liminfresxr  46776  liminfvalxr  46792  liminf0  46802  icccncfext  46896  stoweidlem39  47048  stoweidlem50  47059  stoweidlem57  47066  fourierdlem32  47148  fourierdlem33  47149  fourierdlem48  47163  fourierdlem49  47164  fourierdlem71  47186  sge0rnre  47373  sge00  47385  sge0tsms  47389  sge0cl  47390  sge0fsum  47396  sge0sup  47400  sge0less  47401  sge0gerp  47404  sge0resplit  47415  sge0split  47418  sge0iunmptlemre  47424  caragendifcl  47523  hoiqssbllem3  47633  hspmbllem2  47636  pimiooltgt  47719  pimdecfgtioc  47724  pimincfltioc  47725  pimdecfgtioo  47726  pimincfltioo  47727  sssmf  47747  smfaddlem1  47772  smfaddlem2  47773  smfadd  47774  mbfpsssmf  47792  smfmul  47804  smfdiv  47806  smfsuplem1  47820  smfliminflem  47839  numtowerdt  47915  fmtno4prm  48659  rhmsubcALTVlem3  49379