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 500	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 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  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  6309  fvcofneq  7075  frrlem4  8271  frrlem12  8279  erdisj  8737  f1opwfi  9300  fival  9359  fi0  9367  dffi2  9370  elfiun  9377  epfrs  9687  r0weon  9969  fodomfi2  10017  ackbij1lem6  10181  ackbij1lem9  10184  ackbij1lem10  10185  ackbij1lem11  10186  fin23lem24  10280  fin23lem26  10283  isfin1-3  10344  canthp1lem2  10612  dedekindle  11348  uzdisj  13603  nn0disj  13650  lo1resb  15592  rlimresb  15593  o1resb  15594  ackbijnn  15859  prmreclem2  16954  isacs2  17686  acsfn  17692  isdrs2  18339  isacs3lem  18575  psssdm2  18614  resscntz  19374  rngcid  20686  ringcid  20715  rhmsubclem3  20738  mplind  22124  clsval2  23111  mreclatdemoBAD  23157  ordtrest  23263  fincmp  23454  discmp  23459  uncmp  23464  ptcnplem  23682  txkgen  23713  infil  23924  hauspwpwf1  24048  alexsubALTlem3  24110  alexsubALTlem4  24111  blbas  24491  blres  24492  xrge0tsms  24896  nmhmcn  25183  ncvsge0  25216  cphsscph  25314  mbfadd  25724  mbfsub  25725  i1fima2  25742  i1fd  25744  mbfmul  25789  bddmulibl  25902  limcun  25958  pilem2  26516  rlimcnp2  27032  xrlimcnp  27034  ppiprm  27216  chtprm  27218  prmorcht  27243  rplogsumlem2  27550  dchrisum0re  27578  uhgrspansubgrlem  29492  disjin  32787  xrge0tsmsd  33254  eulerpartgbij  34670  dfttc4  36891  pibt2  37912  dfadjliftmap2  38957  dfblockliftmap2  38961  eqvreldisj  39198  mhpind  43177  fiinfi  44150  gneispace  44711  ismnushort  44878  elpwinss  45630  restuni3  45697  disjinfi  45771  inmap  45786  iocopn  46097  icoopn  46102  icomnfinre  46129  uzinico  46136  islpcn  46214  lptre2pt  46215  limcresiooub  46217  limcresioolb  46218  limsupmnflem  46295  limsupresxr  46341  liminfresxr  46342  liminfvalxr  46358  liminf0  46368  icccncfext  46462  stoweidlem39  46614  stoweidlem50  46625  stoweidlem57  46632  fourierdlem32  46714  fourierdlem33  46715  fourierdlem48  46729  fourierdlem49  46730  fourierdlem71  46752  sge0rnre  46939  sge00  46951  sge0tsms  46955  sge0cl  46956  sge0fsum  46962  sge0sup  46966  sge0less  46967  sge0gerp  46970  sge0resplit  46981  sge0split  46984  sge0iunmptlemre  46990  caragendifcl  47089  hoiqssbllem3  47199  hspmbllem2  47202  pimiooltgt  47285  pimdecfgtioc  47290  pimincfltioc  47291  pimdecfgtioo  47292  pimincfltioo  47293  sssmf  47313  smfaddlem1  47338  smfaddlem2  47339  smfadd  47340  mbfpsssmf  47358  smfmul  47370  smfdiv  47372  smfsuplem1  47386  smfliminflem  47405  nthrucw  47463  fmtno4prm  48185  rhmsubcALTVlem3  48906