Theorem elinel1 4147

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  elin1d  4150  nel1nelin  4153  inss1  4182  predel  6319  fvcofneq  7087  frrlem4  8289  frrlem12  8297  erdisj  8757  f1opwfi  9326  fival  9385  fi0  9393  dffi2  9396  elfiun  9403  epfrs  9713  r0weon  10018  fodomfi2  10066  ackbij1lem6  10229  ackbij1lem9  10232  ackbij1lem10  10233  ackbij1lem11  10234  fin23lem24  10327  fin23lem26  10330  isfin1-3  10391  canthp1lem2  10665  dedekindle  11401  uzdisj  13655  nn0disj  13702  lo1resb  15654  rlimresb  15655  o1resb  15656  ackbijnn  15920  prmreclem2  17012  isacs2  17744  acsfn  17750  isdrs2  18397  isacs3lem  18633  psssdm2  18672  resscntz  19463  rngcid  20800  ringcid  20829  rhmsubclem3  20852  mplind  22289  clsval2  23278  mreclatdemoBAD  23324  ordtrest  23430  fincmp  23621  discmp  23626  uncmp  23631  ptcnplem  23850  txkgen  23881  infil  24092  hauspwpwf1  24216  alexsubALTlem3  24278  alexsubALTlem4  24279  blbas  24659  blres  24660  xrge0tsms  25064  nmhmcn  25351  ncvsge0  25384  cphsscph  25482  mbfadd  25892  mbfsub  25893  i1fima2  25910  i1fd  25912  mbfmul  25957  bddmulibl  26069  limcun  26125  pilem2  26691  rlimcnp2  27206  xrlimcnp  27208  ppiprm  27390  chtprm  27392  prmorcht  27417  rplogsumlem2  27724  dchrisum0re  27752  uhgrspansubgrlem  29753  disjin  33062  xrge0tsmsd  33516  eulerpartgbij  34886  dfttc4  37152  pibt2  38174  dfadjliftmap2  39208  dfblockliftmap2  39212  eqvreldisj  39449  mhpind  43443  fiinfi  44416  gneispace  44977  ismnushort  45128  elpwinss  45886  restuni3  45953  disjinfi  46027  inmap  46042  iocopn  46353  icoopn  46358  icomnfinre  46385  uzinico  46392  islpcn  46470  lptre2pt  46471  limcresiooub  46473  limcresioolb  46474  limsupmnflem  46551  limsupresxr  46597  liminfresxr  46598  liminfvalxr  46614  liminf0  46624  icccncfext  46718  stoweidlem39  46870  stoweidlem50  46881  stoweidlem57  46888  fourierdlem32  46970  fourierdlem33  46971  fourierdlem48  46985  fourierdlem49  46986  fourierdlem71  47008  sge0rnre  47195  sge00  47207  sge0tsms  47211  sge0cl  47212  sge0fsum  47218  sge0sup  47222  sge0less  47223  sge0gerp  47226  sge0resplit  47237  sge0split  47240  sge0iunmptlemre  47246  caragendifcl  47345  hoiqssbllem3  47455  hspmbllem2  47458  pimiooltgt  47541  pimdecfgtioc  47546  pimincfltioc  47547  pimdecfgtioo  47548  pimincfltioo  47549  sssmf  47569  smfaddlem1  47594  smfaddlem2  47595  smfadd  47596  mbfpsssmf  47614  smfmul  47626  smfdiv  47628  smfsuplem1  47642  smfliminflem  47661  numtowerdt  47737  fmtno4prm  48481  rhmsubcALTVlem3  49201