Theorem elinel1 4152

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 497	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)

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

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

This theorem is referenced by:  elin1d  4155  nel1nelin  4158  inss1  4188  predel  6269  fvcofneq  7027  frrlem4  8222  frrlem12  8230  erdisj  8682  f1opwfi  9246  fival  9302  fi0  9310  dffi2  9313  elfiun  9320  epfrs  9627  r0weon  9906  fodomfi2  9954  ackbij1lem6  10118  ackbij1lem9  10121  ackbij1lem10  10122  ackbij1lem11  10123  fin23lem24  10216  fin23lem26  10219  isfin1-3  10280  canthp1lem2  10547  dedekindle  11280  uzdisj  13500  nn0disj  13547  lo1resb  15471  rlimresb  15472  o1resb  15473  ackbijnn  15735  prmreclem2  16829  isacs2  17559  acsfn  17565  isdrs2  18212  isacs3lem  18448  psssdm2  18487  resscntz  19212  rngcid  20520  ringcid  20549  rhmsubclem3  20572  mplind  21975  clsval2  22935  mreclatdemoBAD  22981  ordtrest  23087  fincmp  23278  discmp  23283  uncmp  23288  ptcnplem  23506  txkgen  23537  infil  23748  hauspwpwf1  23872  alexsubALTlem3  23934  alexsubALTlem4  23935  blbas  24316  blres  24317  xrge0tsms  24721  nmhmcn  25018  ncvsge0  25051  cphsscph  25149  mbfadd  25560  mbfsub  25561  i1fima2  25578  i1fd  25580  mbfmul  25625  bddmulibl  25738  limcun  25794  pilem2  26360  rlimcnp2  26874  xrlimcnp  26876  ppiprm  27059  chtprm  27061  prmorcht  27086  rplogsumlem2  27394  dchrisum0re  27422  uhgrspansubgrlem  29235  disjin  32530  xrge0tsmsd  33016  eulerpartgbij  34346  pibt2  37401  eqvreldisj  38601  mhpind  42577  fiinfi  43556  gneispace  44117  ismnushort  44284  elpwinss  45037  restuni3  45106  disjinfi  45180  inmap  45197  iocopn  45511  icoopn  45516  icomnfinre  45543  uzinico  45550  islpcn  45630  lptre2pt  45631  limcresiooub  45633  limcresioolb  45634  limsupmnflem  45711  limsupresxr  45757  liminfresxr  45758  liminfvalxr  45774  liminf0  45784  icccncfext  45878  stoweidlem39  46030  stoweidlem50  46041  stoweidlem57  46048  fourierdlem32  46130  fourierdlem33  46131  fourierdlem48  46145  fourierdlem49  46146  fourierdlem71  46168  sge0rnre  46355  sge00  46367  sge0tsms  46371  sge0cl  46372  sge0fsum  46378  sge0sup  46382  sge0less  46383  sge0gerp  46386  sge0resplit  46397  sge0split  46400  sge0iunmptlemre  46406  caragendifcl  46505  hoiqssbllem3  46615  hspmbllem2  46618  pimiooltgt  46701  pimdecfgtioc  46706  pimincfltioc  46707  pimdecfgtioo  46708  pimincfltioo  46709  sssmf  46729  smfaddlem1  46754  smfaddlem2  46755  smfadd  46756  mbfpsssmf  46774  smfmul  46786  smfdiv  46788  smfsuplem1  46802  smfliminflem  46821  fmtno4prm  47569  rhmsubcALTVlem3  48277