Theorem elinel1 4200

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957

This theorem is referenced by:  elin1d  4203  nel1nelin  4206  inss1  4236  predel  6341  fvcofneq  7112  frrlem4  8315  frrlem12  8323  wfrlem4OLD  8353  erdisj  8800  f1opwfi  9397  fival  9453  fi0  9461  dffi2  9464  elfiun  9471  epfrs  9772  r0weon  10053  fodomfi2  10101  ackbij1lem6  10265  ackbij1lem9  10268  ackbij1lem10  10269  ackbij1lem11  10270  fin23lem24  10363  fin23lem26  10366  isfin1-3  10427  canthp1lem2  10694  dedekindle  11426  uzdisj  13638  nn0disj  13685  lo1resb  15601  rlimresb  15602  o1resb  15603  ackbijnn  15865  prmreclem2  16956  isacs2  17697  acsfn  17703  isdrs2  18353  isacs3lem  18588  psssdm2  18627  resscntz  19352  rngcid  20636  ringcid  20665  rhmsubclem3  20688  mplind  22095  clsval2  23059  mreclatdemoBAD  23105  ordtrest  23211  fincmp  23402  discmp  23407  uncmp  23412  ptcnplem  23630  txkgen  23661  infil  23872  hauspwpwf1  23996  alexsubALTlem3  24058  alexsubALTlem4  24059  blbas  24441  blres  24442  xrge0tsms  24857  nmhmcn  25154  ncvsge0  25188  cphsscph  25286  mbfadd  25697  mbfsub  25698  i1fima2  25715  i1fd  25717  mbfmul  25762  bddmulibl  25875  limcun  25931  pilem2  26497  rlimcnp2  27010  xrlimcnp  27012  ppiprm  27195  chtprm  27197  prmorcht  27222  rplogsumlem2  27530  dchrisum0re  27558  uhgrspansubgrlem  29308  disjin  32600  xrge0tsmsd  33066  eulerpartgbij  34375  pibt2  37419  eqvreldisj  38616  mhpind  42609  fiinfi  43591  gneispace  44152  ismnushort  44325  elpwinss  45059  restuni3  45128  disjinfi  45202  inmap  45219  iocopn  45538  icoopn  45543  icomnfinre  45570  uzinico  45578  islpcn  45659  lptre2pt  45660  limcresiooub  45662  limcresioolb  45663  limsupmnflem  45740  limsupresxr  45786  liminfresxr  45787  liminfvalxr  45803  liminf0  45813  icccncfext  45907  stoweidlem39  46059  stoweidlem50  46070  stoweidlem57  46077  fourierdlem32  46159  fourierdlem33  46160  fourierdlem48  46174  fourierdlem49  46175  fourierdlem71  46197  sge0rnre  46384  sge00  46396  sge0tsms  46400  sge0cl  46401  sge0fsum  46407  sge0sup  46411  sge0less  46412  sge0gerp  46415  sge0resplit  46426  sge0split  46429  sge0iunmptlemre  46435  caragendifcl  46534  hoiqssbllem3  46644  hspmbllem2  46647  pimiooltgt  46730  pimdecfgtioc  46735  pimincfltioc  46736  pimdecfgtioo  46737  pimincfltioo  46738  sssmf  46758  smfaddlem1  46783  smfaddlem2  46784  smfadd  46785  mbfpsssmf  46803  smfmul  46815  smfdiv  46817  smfsuplem1  46831  smfliminflem  46850  fmtno4prm  47567  rhmsubcALTVlem3  48204