Theorem elinel1 4130

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3887

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895

This theorem is referenced by:  elin1d  4133  inss1  4163  predel  6227  fvcofneq  6978  frrlem4  8114  frrlem12  8122  wfrlem4OLD  8152  erdisj  8559  f1opwfi  9132  fival  9180  fi0  9188  dffi2  9191  elfiun  9198  epfrs  9498  r0weon  9777  fodomfi2  9825  ackbij1lem6  9990  ackbij1lem9  9993  ackbij1lem10  9994  ackbij1lem11  9995  fin23lem24  10087  fin23lem26  10090  isfin1-3  10151  canthp1lem2  10418  dedekindle  11148  uzdisj  13338  nn0disj  13381  lo1resb  15282  rlimresb  15283  o1resb  15284  ackbijnn  15549  prmreclem2  16627  isacs2  17371  acsfn  17377  isdrs2  18033  isacs3lem  18269  psssdm2  18308  resscntz  18947  mplind  21287  clsval2  22210  mreclatdemoBAD  22256  ordtrest  22362  fincmp  22553  discmp  22558  uncmp  22563  ptcnplem  22781  txkgen  22812  infil  23023  hauspwpwf1  23147  alexsubALTlem3  23209  alexsubALTlem4  23210  blbas  23592  blres  23593  xrge0tsms  24006  nmhmcn  24292  ncvsge0  24326  cphsscph  24424  mbfadd  24834  mbfsub  24835  i1fima2  24852  i1fd  24854  mbfmul  24900  bddmulibl  25012  limcun  25068  pilem2  25620  rlimcnp2  26125  xrlimcnp  26127  ppiprm  26309  chtprm  26311  prmorcht  26336  rplogsumlem2  26642  dchrisum0re  26670  uhgrspansubgrlem  27666  disjin  30934  xrge0tsmsd  31326  eulerpartgbij  32348  pibt2  35597  eqvreldisj  36734  mhpind  40290  fiinfi  41187  gneispace  41751  ismnushort  41926  elpwinss  42604  restuni3  42674  nel1nelin  42702  disjinfi  42738  inmap  42756  iocopn  43065  icoopn  43070  icomnfinre  43097  uzinico  43105  islpcn  43187  lptre2pt  43188  limcresiooub  43190  limcresioolb  43191  limsupmnflem  43268  limsupresxr  43314  liminfresxr  43315  liminfvalxr  43331  liminf0  43341  icccncfext  43435  stoweidlem39  43587  stoweidlem50  43598  stoweidlem57  43605  fourierdlem32  43687  fourierdlem33  43688  fourierdlem48  43702  fourierdlem49  43703  fourierdlem71  43725  sge0rnre  43909  sge00  43921  sge0tsms  43925  sge0cl  43926  sge0fsum  43932  sge0sup  43936  sge0less  43937  sge0gerp  43940  sge0resplit  43951  sge0split  43954  sge0iunmptlemre  43960  caragendifcl  44059  hoiqssbllem3  44169  hspmbllem2  44172  pimiooltgt  44255  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  sssmf  44283  smfaddlem1  44308  smfaddlem2  44309  smfadd  44310  mbfpsssmf  44328  smfmul  44340  smfdiv  44342  smfsuplem1  44355  smfliminflem  44374  fmtno4prm  45038  rngcid  45548  ringcid  45594  rhmsubclem3  45657  rhmsubcALTVlem3  45675