Theorem elinel1 4101

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  elin1d  4104  nel1nelin  4107  inss1  4136  predel  6331  fvcofneq  7104  frrlem4  8321  frrlem12  8329  erdisj  8789  f1opwfi  9359  fival  9417  fi0  9425  dffi2  9428  elfiun  9435  epfrs  9745  r0weon  10104  fodomfi2  10152  ackbij1lem6  10315  ackbij1lem9  10318  ackbij1lem10  10319  ackbij1lem11  10320  fin23lem24  10413  fin23lem26  10416  isfin1-3  10477  canthp1lem2  10751  dedekindle  11487  uzdisj  13744  nn0disj  13791  lo1resb  15746  rlimresb  15747  o1resb  15748  ackbijnn  16012  prmreclem2  17110  isacs2  17842  acsfn  17848  isdrs2  18495  isacs3lem  18731  psssdm2  18770  resscntz  19562  rngcid  20902  ringcid  20931  rhmsubclem3  20954  mplind  22394  clsval2  23383  mreclatdemoBAD  23429  ordtrest  23535  fincmp  23726  discmp  23731  uncmp  23736  ptcnplem  23955  txkgen  23986  infil  24197  hauspwpwf1  24321  alexsubALTlem3  24383  alexsubALTlem4  24384  blbas  24764  blres  24765  xrge0tsms  25169  nmhmcn  25456  ncvsge0  25489  cphsscph  25587  mbfadd  25997  mbfsub  25998  i1fima2  26015  i1fd  26017  mbfmul  26062  bddmulibl  26174  limcun  26230  pilem2  26794  rlimcnp2  27309  xrlimcnp  27311  ppiprm  27493  chtprm  27495  prmorcht  27520  rplogsumlem2  27827  dchrisum0re  27855  uhgrspansubgrlem  29886  disjin  33237  xrge0tsmsd  33690  eulerpartgbij  35060  dfttc4  37448  pibt2  38483  dfadjliftmap2  39532  dfblockliftmap2  39536  eqvreldisj  39773  mhpind  43765  fiinfi  44717  gneispace  45277  ismnushort  45428  hfstructstruct  46167  elpwinss  46208  restuni3  46275  disjinfi  46349  inmap  46364  iocopn  46674  icoopn  46679  icomnfinre  46706  uzinico  46713  islpcn  46791  lptre2pt  46792  limcresiooub  46794  limcresioolb  46795  limsupmnflem  46872  limsupresxr  46918  liminfresxr  46919  liminfvalxr  46935  liminf0  46945  icccncfext  47039  stoweidlem39  47191  stoweidlem50  47202  stoweidlem57  47209  fourierdlem32  47291  fourierdlem33  47292  fourierdlem48  47306  fourierdlem49  47307  fourierdlem71  47329  sge0rnre  47516  sge00  47528  sge0tsms  47532  sge0cl  47533  sge0fsum  47539  sge0sup  47543  sge0less  47544  sge0gerp  47547  sge0resplit  47558  sge0split  47561  sge0iunmptlemre  47567  caragendifcl  47666  hoiqssbllem3  47776  hspmbllem2  47779  pimiooltgt  47862  pimdecfgtioc  47867  pimincfltioc  47868  pimdecfgtioo  47869  pimincfltioo  47870  sssmf  47890  smfaddlem1  47915  smfaddlem2  47916  smfadd  47917  mbfpsssmf  47935  smfmul  47947  smfdiv  47949  smfsuplem1  47963  smfliminflem  47982  numtowerdt  48058  fmtno4prm  48802  rhmsubcALTVlem3  49522