Theorem elinel1 4195

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955

This theorem is referenced by:  elin1d  4198  inss1  4228  predel  6321  fvcofneq  7094  frrlem4  8276  frrlem12  8284  wfrlem4OLD  8314  erdisj  8757  f1opwfi  9358  fival  9409  fi0  9417  dffi2  9420  elfiun  9427  epfrs  9728  r0weon  10009  fodomfi2  10057  ackbij1lem6  10222  ackbij1lem9  10225  ackbij1lem10  10226  ackbij1lem11  10227  fin23lem24  10319  fin23lem26  10322  isfin1-3  10383  canthp1lem2  10650  dedekindle  11382  uzdisj  13578  nn0disj  13621  lo1resb  15512  rlimresb  15513  o1resb  15514  ackbijnn  15778  prmreclem2  16854  isacs2  17601  acsfn  17607  isdrs2  18263  isacs3lem  18499  psssdm2  18538  resscntz  19238  mplind  21850  clsval2  22774  mreclatdemoBAD  22820  ordtrest  22926  fincmp  23117  discmp  23122  uncmp  23127  ptcnplem  23345  txkgen  23376  infil  23587  hauspwpwf1  23711  alexsubALTlem3  23773  alexsubALTlem4  23774  blbas  24156  blres  24157  xrge0tsms  24570  nmhmcn  24860  ncvsge0  24894  cphsscph  24992  mbfadd  25402  mbfsub  25403  i1fima2  25420  i1fd  25422  mbfmul  25468  bddmulibl  25580  limcun  25636  pilem2  26188  rlimcnp2  26695  xrlimcnp  26697  ppiprm  26879  chtprm  26881  prmorcht  26906  rplogsumlem2  27212  dchrisum0re  27240  uhgrspansubgrlem  28802  disjin  32072  xrge0tsmsd  32467  eulerpartgbij  33657  pibt2  36601  eqvreldisj  37787  mhpind  41468  fiinfi  42626  gneispace  43187  ismnushort  43362  elpwinss  44038  restuni3  44109  nel1nelin  44137  disjinfi  44190  inmap  44207  iocopn  44532  icoopn  44537  icomnfinre  44564  uzinico  44572  islpcn  44654  lptre2pt  44655  limcresiooub  44657  limcresioolb  44658  limsupmnflem  44735  limsupresxr  44781  liminfresxr  44782  liminfvalxr  44798  liminf0  44808  icccncfext  44902  stoweidlem39  45054  stoweidlem50  45065  stoweidlem57  45072  fourierdlem32  45154  fourierdlem33  45155  fourierdlem48  45169  fourierdlem49  45170  fourierdlem71  45192  sge0rnre  45379  sge00  45391  sge0tsms  45395  sge0cl  45396  sge0fsum  45402  sge0sup  45406  sge0less  45407  sge0gerp  45410  sge0resplit  45421  sge0split  45424  sge0iunmptlemre  45430  caragendifcl  45529  hoiqssbllem3  45639  hspmbllem2  45642  pimiooltgt  45725  pimdecfgtioc  45730  pimincfltioc  45731  pimdecfgtioo  45732  pimincfltioo  45733  sssmf  45753  smfaddlem1  45778  smfaddlem2  45779  smfadd  45780  mbfpsssmf  45798  smfmul  45810  smfdiv  45812  smfsuplem1  45826  smfliminflem  45845  fmtno4prm  46542  rngcid  46966  ringcid  47012  rhmsubclem3  47075  rhmsubcALTVlem3  47093