Theorem elinel1 4194

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3946

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954

This theorem is referenced by:  elin1d  4197  inss1  4227  predel  6318  fvcofneq  7091  frrlem4  8270  frrlem12  8278  wfrlem4OLD  8308  erdisj  8751  f1opwfi  9352  fival  9403  fi0  9411  dffi2  9414  elfiun  9421  epfrs  9722  r0weon  10003  fodomfi2  10051  ackbij1lem6  10216  ackbij1lem9  10219  ackbij1lem10  10220  ackbij1lem11  10221  fin23lem24  10313  fin23lem26  10316  isfin1-3  10377  canthp1lem2  10644  dedekindle  11374  uzdisj  13570  nn0disj  13613  lo1resb  15504  rlimresb  15505  o1resb  15506  ackbijnn  15770  prmreclem2  16846  isacs2  17593  acsfn  17599  isdrs2  18255  isacs3lem  18491  psssdm2  18530  resscntz  19191  mplind  21622  clsval2  22545  mreclatdemoBAD  22591  ordtrest  22697  fincmp  22888  discmp  22893  uncmp  22898  ptcnplem  23116  txkgen  23147  infil  23358  hauspwpwf1  23482  alexsubALTlem3  23544  alexsubALTlem4  23545  blbas  23927  blres  23928  xrge0tsms  24341  nmhmcn  24627  ncvsge0  24661  cphsscph  24759  mbfadd  25169  mbfsub  25170  i1fima2  25187  i1fd  25189  mbfmul  25235  bddmulibl  25347  limcun  25403  pilem2  25955  rlimcnp2  26460  xrlimcnp  26462  ppiprm  26644  chtprm  26646  prmorcht  26671  rplogsumlem2  26977  dchrisum0re  27005  uhgrspansubgrlem  28536  disjin  31804  xrge0tsmsd  32196  eulerpartgbij  33359  pibt2  36286  eqvreldisj  37472  mhpind  41163  fiinfi  42309  gneispace  42870  ismnushort  43045  elpwinss  43721  restuni3  43792  nel1nelin  43820  disjinfi  43876  inmap  43893  iocopn  44219  icoopn  44224  icomnfinre  44251  uzinico  44259  islpcn  44341  lptre2pt  44342  limcresiooub  44344  limcresioolb  44345  limsupmnflem  44422  limsupresxr  44468  liminfresxr  44469  liminfvalxr  44485  liminf0  44495  icccncfext  44589  stoweidlem39  44741  stoweidlem50  44752  stoweidlem57  44759  fourierdlem32  44841  fourierdlem33  44842  fourierdlem48  44856  fourierdlem49  44857  fourierdlem71  44879  sge0rnre  45066  sge00  45078  sge0tsms  45082  sge0cl  45083  sge0fsum  45089  sge0sup  45093  sge0less  45094  sge0gerp  45097  sge0resplit  45108  sge0split  45111  sge0iunmptlemre  45117  caragendifcl  45216  hoiqssbllem3  45326  hspmbllem2  45329  pimiooltgt  45412  pimdecfgtioc  45417  pimincfltioc  45418  pimdecfgtioo  45419  pimincfltioo  45420  sssmf  45440  smfaddlem1  45465  smfaddlem2  45466  smfadd  45467  mbfpsssmf  45485  smfmul  45497  smfdiv  45499  smfsuplem1  45513  smfliminflem  45532  fmtno4prm  46229  rngcid  46830  ringcid  46876  rhmsubclem3  46939  rhmsubcALTVlem3  46957