Theorem elinel1 4154

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

Syntax hints:   → wi 4   ∈ wcel 2143   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  elin1d  4157  nel1nelin  4160  inss1  4189  predel  6322  fvcofneq  7088  frrlem4  8282  frrlem12  8290  erdisj  8748  f1opwfi  9309  fival  9368  fi0  9376  dffi2  9379  elfiun  9386  epfrs  9696  r0weon  9992  fodomfi2  10040  ackbij1lem6  10203  ackbij1lem9  10206  ackbij1lem10  10207  ackbij1lem11  10208  fin23lem24  10301  fin23lem26  10304  isfin1-3  10365  canthp1lem2  10633  dedekindle  11369  uzdisj  13621  nn0disj  13668  lo1resb  15611  rlimresb  15612  o1resb  15613  ackbijnn  15878  prmreclem2  16972  isacs2  17704  acsfn  17710  isdrs2  18357  isacs3lem  18593  psssdm2  18632  resscntz  19398  rngcid  20734  ringcid  20763  rhmsubclem3  20786  mplind  22221  clsval2  23207  mreclatdemoBAD  23253  ordtrest  23359  fincmp  23550  discmp  23555  uncmp  23560  ptcnplem  23778  txkgen  23809  infil  24020  hauspwpwf1  24144  alexsubALTlem3  24206  alexsubALTlem4  24207  blbas  24587  blres  24588  xrge0tsms  24992  nmhmcn  25279  ncvsge0  25312  cphsscph  25410  mbfadd  25820  mbfsub  25821  i1fima2  25838  i1fd  25840  mbfmul  25885  bddmulibl  25998  limcun  26054  pilem2  26615  rlimcnp2  27131  xrlimcnp  27133  ppiprm  27315  chtprm  27317  prmorcht  27342  rplogsumlem2  27649  dchrisum0re  27677  uhgrspansubgrlem  29640  disjin  32931  xrge0tsmsd  33393  eulerpartgbij  34762  dfttc4  37061  pibt2  38083  dfadjliftmap2  39126  dfblockliftmap2  39130  eqvreldisj  39367  mhpind  43346  fiinfi  44319  gneispace  44880  ismnushort  45031  elpwinss  45789  restuni3  45856  disjinfi  45930  inmap  45945  iocopn  46256  icoopn  46261  icomnfinre  46288  uzinico  46295  islpcn  46373  lptre2pt  46374  limcresiooub  46376  limcresioolb  46377  limsupmnflem  46454  limsupresxr  46500  liminfresxr  46501  liminfvalxr  46517  liminf0  46527  icccncfext  46621  stoweidlem39  46773  stoweidlem50  46784  stoweidlem57  46791  fourierdlem32  46873  fourierdlem33  46874  fourierdlem48  46888  fourierdlem49  46889  fourierdlem71  46911  sge0rnre  47098  sge00  47110  sge0tsms  47114  sge0cl  47115  sge0fsum  47121  sge0sup  47125  sge0less  47126  sge0gerp  47129  sge0resplit  47140  sge0split  47143  sge0iunmptlemre  47149  caragendifcl  47248  hoiqssbllem3  47358  hspmbllem2  47361  pimiooltgt  47444  pimdecfgtioc  47449  pimincfltioc  47450  pimdecfgtioo  47451  pimincfltioo  47452  sssmf  47472  smfaddlem1  47497  smfaddlem2  47498  smfadd  47499  mbfpsssmf  47517  smfmul  47529  smfdiv  47531  smfsuplem1  47545  smfliminflem  47564  nthrucw  47627  fmtno4prm  48347  rhmsubcALTVlem3  49068