Theorem elinel1 3761

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

Syntax hints:   → wi 4   ∈ wcel 1977   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  elin1d  3764  inss1  3795  predel  5614  prmreclem2  15459  txkgen  21265  ncvsge0  22761  dchrisum0re  25002  xrge0tsmsd  29116  eulerpartgbij  29761  fiinfi  36897  gneispace  37452  elpwinss  38241  restuni3  38333  disjinfi  38375  inmap  38396  iocopn  38593  icoopn  38598  icomnfinre  38626  islpcn  38706  lptre2pt  38707  limcresiooub  38709  limcresioolb  38710  icccncfext  38773  stoweidlem39  38932  stoweidlem50  38943  stoweidlem57  38950  fourierdlem32  39032  fourierdlem33  39033  fourierdlem48  39047  fourierdlem49  39048  fourierdlem71  39070  sge0rnre  39257  sge00  39269  sge0tsms  39273  sge0cl  39274  sge0fsum  39280  sge0sup  39284  sge0less  39285  sge0gerp  39288  sge0resplit  39299  sge0split  39302  sge0iunmptlemre  39308  caragendifcl  39404  hoiqssbllem3  39514  hspmbllem2  39517  pimiooltgt  39598  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  sssmf  39625  smfaddlem1  39649  smfaddlem2  39650  smfadd  39651  mbfpsssmf  39669  smfmul  39680  smfdiv  39682  fmtno4prm  40025  uhgrspansubgrlem  40514  rngcid  41771  ringcid  41817  rhmsubclem3  41880  rhmsubcALTVlem3  41899