Theorem elinel1 4131

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

Syntax hints:   → wi 4   ∈ wcel 2119   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  elin1d  4134  nel1nelin  4137  inss1  4166  predel  6273  fvcofneq  7035  frrlem4  8230  frrlem12  8238  erdisj  8692  f1opwfi  9257  fival  9316  fi0  9324  dffi2  9327  elfiun  9334  epfrs  9644  r0weon  9926  fodomfi2  9974  ackbij1lem6  10138  ackbij1lem9  10141  ackbij1lem10  10142  ackbij1lem11  10143  fin23lem24  10236  fin23lem26  10239  isfin1-3  10300  canthp1lem2  10568  dedekindle  11302  uzdisj  13543  nn0disj  13590  lo1resb  15518  rlimresb  15519  o1resb  15520  ackbijnn  15785  prmreclem2  16880  isacs2  17611  acsfn  17617  isdrs2  18264  isacs3lem  18500  psssdm2  18539  resscntz  19300  rngcid  20608  ringcid  20637  rhmsubclem3  20660  mplind  22047  clsval2  23034  mreclatdemoBAD  23080  ordtrest  23186  fincmp  23377  discmp  23382  uncmp  23387  ptcnplem  23605  txkgen  23636  infil  23847  hauspwpwf1  23971  alexsubALTlem3  24033  alexsubALTlem4  24034  blbas  24414  blres  24415  xrge0tsms  24819  nmhmcn  25106  ncvsge0  25139  cphsscph  25237  mbfadd  25647  mbfsub  25648  i1fima2  25665  i1fd  25667  mbfmul  25712  bddmulibl  25825  limcun  25881  pilem2  26436  rlimcnp2  26949  xrlimcnp  26951  ppiprm  27133  chtprm  27135  prmorcht  27160  rplogsumlem2  27467  dchrisum0re  27495  uhgrspansubgrlem  29378  disjin  32676  xrge0tsmsd  33155  eulerpartgbij  34565  dfttc4  36767  pibt2  37788  dfadjliftmap2  38833  dfblockliftmap2  38837  eqvreldisj  39074  mhpind  43053  fiinfi  44026  gneispace  44587  ismnushort  44754  elpwinss  45506  restuni3  45573  disjinfi  45647  inmap  45662  iocopn  45973  icoopn  45978  icomnfinre  46005  uzinico  46012  islpcn  46090  lptre2pt  46091  limcresiooub  46093  limcresioolb  46094  limsupmnflem  46171  limsupresxr  46217  liminfresxr  46218  liminfvalxr  46234  liminf0  46244  icccncfext  46338  stoweidlem39  46490  stoweidlem50  46501  stoweidlem57  46508  fourierdlem32  46590  fourierdlem33  46591  fourierdlem48  46605  fourierdlem49  46606  fourierdlem71  46628  sge0rnre  46815  sge00  46827  sge0tsms  46831  sge0cl  46832  sge0fsum  46838  sge0sup  46842  sge0less  46843  sge0gerp  46846  sge0resplit  46857  sge0split  46860  sge0iunmptlemre  46866  caragendifcl  46965  hoiqssbllem3  47075  hspmbllem2  47078  pimiooltgt  47161  pimdecfgtioc  47166  pimincfltioc  47167  pimdecfgtioo  47168  pimincfltioo  47169  sssmf  47189  smfaddlem1  47214  smfaddlem2  47215  smfadd  47216  mbfpsssmf  47234  smfmul  47246  smfdiv  47248  smfsuplem1  47262  smfliminflem  47281  nthrucw  47339  fmtno4prm  48061  rhmsubcALTVlem3  48782