Theorem elinel1 4109

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

Syntax hints:   → wi 4   ∈ wcel 2110   ∩ cin 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873

This theorem is referenced by:  elin1d  4112  inss1  4143  predel  6179  fvcofneq  6912  frrlem4  8030  frrlem12  8038  wfrlem4  8058  erdisj  8443  f1opwfi  8980  fival  9028  fi0  9036  dffi2  9039  elfiun  9046  epfrs  9347  r0weon  9626  fodomfi2  9674  ackbij1lem6  9839  ackbij1lem9  9842  ackbij1lem10  9843  ackbij1lem11  9844  fin23lem24  9936  fin23lem26  9939  isfin1-3  10000  canthp1lem2  10267  dedekindle  10996  uzdisj  13185  nn0disj  13228  lo1resb  15125  rlimresb  15126  o1resb  15127  ackbijnn  15392  prmreclem2  16470  isacs2  17156  acsfn  17162  isdrs2  17813  isacs3lem  18048  psssdm2  18087  resscntz  18726  mplind  21028  clsval2  21947  mreclatdemoBAD  21993  ordtrest  22099  fincmp  22290  discmp  22295  uncmp  22300  ptcnplem  22518  txkgen  22549  infil  22760  hauspwpwf1  22884  alexsubALTlem3  22946  alexsubALTlem4  22947  blbas  23328  blres  23329  xrge0tsms  23731  nmhmcn  24017  ncvsge0  24050  cphsscph  24148  mbfadd  24558  mbfsub  24559  i1fima2  24576  i1fd  24578  mbfmul  24624  bddmulibl  24736  limcun  24792  pilem2  25344  rlimcnp2  25849  xrlimcnp  25851  ppiprm  26033  chtprm  26035  prmorcht  26060  rplogsumlem2  26366  dchrisum0re  26394  uhgrspansubgrlem  27378  disjin  30644  xrge0tsmsd  31036  eulerpartgbij  32051  pibt2  35325  eqvreldisj  36464  mhpind  39993  fiinfi  40856  gneispace  41421  ismnushort  41592  elpwinss  42270  restuni3  42340  nel1nelin  42368  disjinfi  42404  inmap  42422  iocopn  42733  icoopn  42738  icomnfinre  42765  uzinico  42773  islpcn  42855  lptre2pt  42856  limcresiooub  42858  limcresioolb  42859  limsupmnflem  42936  limsupresxr  42982  liminfresxr  42983  liminfvalxr  42999  liminf0  43009  icccncfext  43103  stoweidlem39  43255  stoweidlem50  43266  stoweidlem57  43273  fourierdlem32  43355  fourierdlem33  43356  fourierdlem48  43370  fourierdlem49  43371  fourierdlem71  43393  sge0rnre  43577  sge00  43589  sge0tsms  43593  sge0cl  43594  sge0fsum  43600  sge0sup  43604  sge0less  43605  sge0gerp  43608  sge0resplit  43619  sge0split  43622  sge0iunmptlemre  43628  caragendifcl  43727  hoiqssbllem3  43837  hspmbllem2  43840  pimiooltgt  43920  pimdecfgtioc  43924  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  sssmf  43946  smfaddlem1  43970  smfaddlem2  43971  smfadd  43972  mbfpsssmf  43990  smfmul  44001  smfdiv  44003  smfsuplem1  44016  smfliminflem  44035  fmtno4prm  44700  rngcid  45210  ringcid  45256  rhmsubclem3  45319  rhmsubcALTVlem3  45337