Theorem elinel1 4155

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

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

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 3444  df-in 3910

This theorem is referenced by:  elin1d  4158  nel1nelin  4161  inss1  4191  predel  6287  fvcofneq  7047  frrlem4  8241  frrlem12  8249  erdisj  8703  f1opwfi  9268  fival  9327  fi0  9335  dffi2  9338  elfiun  9345  epfrs  9652  r0weon  9934  fodomfi2  9982  ackbij1lem6  10146  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1lem11  10151  fin23lem24  10244  fin23lem26  10247  isfin1-3  10308  canthp1lem2  10576  dedekindle  11309  uzdisj  13525  nn0disj  13572  lo1resb  15499  rlimresb  15500  o1resb  15501  ackbijnn  15763  prmreclem2  16857  isacs2  17588  acsfn  17594  isdrs2  18241  isacs3lem  18477  psssdm2  18516  resscntz  19277  rngcid  20583  ringcid  20612  rhmsubclem3  20635  mplind  22040  clsval2  23009  mreclatdemoBAD  23055  ordtrest  23161  fincmp  23352  discmp  23357  uncmp  23362  ptcnplem  23580  txkgen  23611  infil  23822  hauspwpwf1  23946  alexsubALTlem3  24008  alexsubALTlem4  24009  blbas  24389  blres  24390  xrge0tsms  24794  nmhmcn  25091  ncvsge0  25124  cphsscph  25222  mbfadd  25633  mbfsub  25634  i1fima2  25651  i1fd  25653  mbfmul  25698  bddmulibl  25811  limcun  25867  pilem2  26433  rlimcnp2  26947  xrlimcnp  26949  ppiprm  27132  chtprm  27134  prmorcht  27159  rplogsumlem2  27467  dchrisum0re  27495  uhgrspansubgrlem  29379  disjin  32677  xrge0tsmsd  33171  eulerpartgbij  34554  pibt2  37676  dfadjliftmap2  38712  dfblockliftmap2  38716  eqvreldisj  38953  mhpind  42956  fiinfi  43933  gneispace  44494  ismnushort  44661  elpwinss  45413  restuni3  45481  disjinfi  45555  inmap  45571  iocopn  45884  icoopn  45889  icomnfinre  45916  uzinico  45923  islpcn  46001  lptre2pt  46002  limcresiooub  46004  limcresioolb  46005  limsupmnflem  46082  limsupresxr  46128  liminfresxr  46129  liminfvalxr  46145  liminf0  46155  icccncfext  46249  stoweidlem39  46401  stoweidlem50  46412  stoweidlem57  46419  fourierdlem32  46501  fourierdlem33  46502  fourierdlem48  46516  fourierdlem49  46517  fourierdlem71  46539  sge0rnre  46726  sge00  46738  sge0tsms  46742  sge0cl  46743  sge0fsum  46749  sge0sup  46753  sge0less  46754  sge0gerp  46757  sge0resplit  46768  sge0split  46771  sge0iunmptlemre  46777  caragendifcl  46876  hoiqssbllem3  46986  hspmbllem2  46989  pimiooltgt  47072  pimdecfgtioc  47077  pimincfltioc  47078  pimdecfgtioo  47079  pimincfltioo  47080  sssmf  47100  smfaddlem1  47125  smfaddlem2  47126  smfadd  47127  mbfpsssmf  47145  smfmul  47157  smfdiv  47159  smfsuplem1  47173  smfliminflem  47192  nthrucw  47248  fmtno4prm  47939  rhmsubcALTVlem3  48647