Theorem elinel1 4164

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921

This theorem is referenced by:  elin1d  4167  nel1nelin  4170  inss1  4200  predel  6294  fvcofneq  7065  frrlem4  8268  frrlem12  8276  erdisj  8728  f1opwfi  9307  fival  9363  fi0  9371  dffi2  9374  elfiun  9381  epfrs  9684  r0weon  9965  fodomfi2  10013  ackbij1lem6  10177  ackbij1lem9  10180  ackbij1lem10  10181  ackbij1lem11  10182  fin23lem24  10275  fin23lem26  10278  isfin1-3  10339  canthp1lem2  10606  dedekindle  11338  uzdisj  13558  nn0disj  13605  lo1resb  15530  rlimresb  15531  o1resb  15532  ackbijnn  15794  prmreclem2  16888  isacs2  17614  acsfn  17620  isdrs2  18267  isacs3lem  18501  psssdm2  18540  resscntz  19265  rngcid  20544  ringcid  20573  rhmsubclem3  20596  mplind  21977  clsval2  22937  mreclatdemoBAD  22983  ordtrest  23089  fincmp  23280  discmp  23285  uncmp  23290  ptcnplem  23508  txkgen  23539  infil  23750  hauspwpwf1  23874  alexsubALTlem3  23936  alexsubALTlem4  23937  blbas  24318  blres  24319  xrge0tsms  24723  nmhmcn  25020  ncvsge0  25053  cphsscph  25151  mbfadd  25562  mbfsub  25563  i1fima2  25580  i1fd  25582  mbfmul  25627  bddmulibl  25740  limcun  25796  pilem2  26362  rlimcnp2  26876  xrlimcnp  26878  ppiprm  27061  chtprm  27063  prmorcht  27088  rplogsumlem2  27396  dchrisum0re  27424  uhgrspansubgrlem  29217  disjin  32515  xrge0tsmsd  33002  eulerpartgbij  34363  pibt2  37405  eqvreldisj  38605  mhpind  42582  fiinfi  43562  gneispace  44123  ismnushort  44290  elpwinss  45043  restuni3  45112  disjinfi  45186  inmap  45203  iocopn  45518  icoopn  45523  icomnfinre  45550  uzinico  45557  islpcn  45637  lptre2pt  45638  limcresiooub  45640  limcresioolb  45641  limsupmnflem  45718  limsupresxr  45764  liminfresxr  45765  liminfvalxr  45781  liminf0  45791  icccncfext  45885  stoweidlem39  46037  stoweidlem50  46048  stoweidlem57  46055  fourierdlem32  46137  fourierdlem33  46138  fourierdlem48  46152  fourierdlem49  46153  fourierdlem71  46175  sge0rnre  46362  sge00  46374  sge0tsms  46378  sge0cl  46379  sge0fsum  46385  sge0sup  46389  sge0less  46390  sge0gerp  46393  sge0resplit  46404  sge0split  46407  sge0iunmptlemre  46413  caragendifcl  46512  hoiqssbllem3  46622  hspmbllem2  46625  pimiooltgt  46708  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  sssmf  46736  smfaddlem1  46761  smfaddlem2  46762  smfadd  46763  mbfpsssmf  46781  smfmul  46793  smfdiv  46795  smfsuplem1  46809  smfliminflem  46828  fmtno4prm  47576  rhmsubcALTVlem3  48271