Theorem elinel1 4142

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  elin1d  4145  nel1nelin  4148  inss1  4178  predel  6277  fvcofneq  7037  frrlem4  8230  frrlem12  8238  erdisj  8692  f1opwfi  9257  fival  9316  fi0  9324  dffi2  9327  elfiun  9334  epfrs  9641  r0weon  9923  fodomfi2  9971  ackbij1lem6  10135  ackbij1lem9  10138  ackbij1lem10  10139  ackbij1lem11  10140  fin23lem24  10233  fin23lem26  10236  isfin1-3  10297  canthp1lem2  10565  dedekindle  11299  uzdisj  13540  nn0disj  13587  lo1resb  15515  rlimresb  15516  o1resb  15517  ackbijnn  15782  prmreclem2  16877  isacs2  17608  acsfn  17614  isdrs2  18261  isacs3lem  18497  psssdm2  18536  resscntz  19297  rngcid  20601  ringcid  20630  rhmsubclem3  20653  mplind  22057  clsval2  23024  mreclatdemoBAD  23070  ordtrest  23176  fincmp  23367  discmp  23372  uncmp  23377  ptcnplem  23595  txkgen  23626  infil  23837  hauspwpwf1  23961  alexsubALTlem3  24023  alexsubALTlem4  24024  blbas  24404  blres  24405  xrge0tsms  24809  nmhmcn  25096  ncvsge0  25129  cphsscph  25227  mbfadd  25637  mbfsub  25638  i1fima2  25655  i1fd  25657  mbfmul  25702  bddmulibl  25815  limcun  25871  pilem2  26433  rlimcnp2  26947  xrlimcnp  26949  ppiprm  27132  chtprm  27134  prmorcht  27159  rplogsumlem2  27467  dchrisum0re  27495  uhgrspansubgrlem  29378  disjin  32676  xrge0tsmsd  33154  eulerpartgbij  34537  dfttc4  36733  pibt2  37744  dfadjliftmap2  38789  dfblockliftmap2  38793  eqvreldisj  39030  mhpind  43038  fiinfi  44015  gneispace  44576  ismnushort  44743  elpwinss  45495  restuni3  45563  disjinfi  45637  inmap  45653  iocopn  45965  icoopn  45970  icomnfinre  45997  uzinico  46004  islpcn  46082  lptre2pt  46083  limcresiooub  46085  limcresioolb  46086  limsupmnflem  46163  limsupresxr  46209  liminfresxr  46210  liminfvalxr  46226  liminf0  46236  icccncfext  46330  stoweidlem39  46482  stoweidlem50  46493  stoweidlem57  46500  fourierdlem32  46582  fourierdlem33  46583  fourierdlem48  46597  fourierdlem49  46598  fourierdlem71  46620  sge0rnre  46807  sge00  46819  sge0tsms  46823  sge0cl  46824  sge0fsum  46830  sge0sup  46834  sge0less  46835  sge0gerp  46838  sge0resplit  46849  sge0split  46852  sge0iunmptlemre  46858  caragendifcl  46957  hoiqssbllem3  47067  hspmbllem2  47070  pimiooltgt  47153  pimdecfgtioc  47158  pimincfltioc  47159  pimdecfgtioo  47160  pimincfltioo  47161  sssmf  47181  smfaddlem1  47206  smfaddlem2  47207  smfadd  47208  mbfpsssmf  47226  smfmul  47238  smfdiv  47240  smfsuplem1  47254  smfliminflem  47273  nthrucw  47329  fmtno4prm  48035  rhmsubcALTVlem3  48756