Theorem elinel1 4153

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  elin1d  4156  nel1nelin  4159  inss1  4189  predel  6279  fvcofneq  7038  frrlem4  8231  frrlem12  8239  erdisj  8693  f1opwfi  9258  fival  9317  fi0  9325  dffi2  9328  elfiun  9335  epfrs  9642  r0weon  9924  fodomfi2  9972  ackbij1lem6  10136  ackbij1lem9  10139  ackbij1lem10  10140  ackbij1lem11  10141  fin23lem24  10234  fin23lem26  10237  isfin1-3  10298  canthp1lem2  10566  dedekindle  11299  uzdisj  13515  nn0disj  13562  lo1resb  15489  rlimresb  15490  o1resb  15491  ackbijnn  15753  prmreclem2  16847  isacs2  17578  acsfn  17584  isdrs2  18231  isacs3lem  18467  psssdm2  18506  resscntz  19264  rngcid  20570  ringcid  20599  rhmsubclem3  20622  mplind  22027  clsval2  22996  mreclatdemoBAD  23042  ordtrest  23148  fincmp  23339  discmp  23344  uncmp  23349  ptcnplem  23567  txkgen  23598  infil  23809  hauspwpwf1  23933  alexsubALTlem3  23995  alexsubALTlem4  23996  blbas  24376  blres  24377  xrge0tsms  24781  nmhmcn  25078  ncvsge0  25111  cphsscph  25209  mbfadd  25620  mbfsub  25621  i1fima2  25638  i1fd  25640  mbfmul  25685  bddmulibl  25798  limcun  25854  pilem2  26420  rlimcnp2  26934  xrlimcnp  26936  ppiprm  27119  chtprm  27121  prmorcht  27146  rplogsumlem2  27454  dchrisum0re  27482  uhgrspansubgrlem  29365  disjin  32663  xrge0tsmsd  33157  eulerpartgbij  34531  pibt2  37624  dfadjliftmap2  38654  dfblockliftmap2  38657  eqvreldisj  38893  mhpind  42858  fiinfi  43835  gneispace  44396  ismnushort  44563  elpwinss  45315  restuni3  45383  disjinfi  45457  inmap  45474  iocopn  45787  icoopn  45792  icomnfinre  45819  uzinico  45826  islpcn  45904  lptre2pt  45905  limcresiooub  45907  limcresioolb  45908  limsupmnflem  45985  limsupresxr  46031  liminfresxr  46032  liminfvalxr  46048  liminf0  46058  icccncfext  46152  stoweidlem39  46304  stoweidlem50  46315  stoweidlem57  46322  fourierdlem32  46404  fourierdlem33  46405  fourierdlem48  46419  fourierdlem49  46420  fourierdlem71  46442  sge0rnre  46629  sge00  46641  sge0tsms  46645  sge0cl  46646  sge0fsum  46652  sge0sup  46656  sge0less  46657  sge0gerp  46660  sge0resplit  46671  sge0split  46674  sge0iunmptlemre  46680  caragendifcl  46779  hoiqssbllem3  46889  hspmbllem2  46892  pimiooltgt  46975  pimdecfgtioc  46980  pimincfltioc  46981  pimdecfgtioo  46982  pimincfltioo  46983  sssmf  47003  smfaddlem1  47028  smfaddlem2  47029  smfadd  47030  mbfpsssmf  47048  smfmul  47060  smfdiv  47062  smfsuplem1  47076  smfliminflem  47095  nthrucw  47151  fmtno4prm  47842  rhmsubcALTVlem3  48550