Theorem elinel1 4211

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970

This theorem is referenced by:  elin1d  4214  inss1  4245  predel  6344  fvcofneq  7113  frrlem4  8313  frrlem12  8321  wfrlem4OLD  8351  erdisj  8798  f1opwfi  9394  fival  9450  fi0  9458  dffi2  9461  elfiun  9468  epfrs  9769  r0weon  10050  fodomfi2  10098  ackbij1lem6  10262  ackbij1lem9  10265  ackbij1lem10  10266  ackbij1lem11  10267  fin23lem24  10360  fin23lem26  10363  isfin1-3  10424  canthp1lem2  10691  dedekindle  11423  uzdisj  13634  nn0disj  13681  lo1resb  15597  rlimresb  15598  o1resb  15599  ackbijnn  15861  prmreclem2  16951  isacs2  17698  acsfn  17704  isdrs2  18364  isacs3lem  18600  psssdm2  18639  resscntz  19364  rngcid  20652  ringcid  20681  rhmsubclem3  20704  mplind  22112  clsval2  23074  mreclatdemoBAD  23120  ordtrest  23226  fincmp  23417  discmp  23422  uncmp  23427  ptcnplem  23645  txkgen  23676  infil  23887  hauspwpwf1  24011  alexsubALTlem3  24073  alexsubALTlem4  24074  blbas  24456  blres  24457  xrge0tsms  24870  nmhmcn  25167  ncvsge0  25201  cphsscph  25299  mbfadd  25710  mbfsub  25711  i1fima2  25728  i1fd  25730  mbfmul  25776  bddmulibl  25889  limcun  25945  pilem2  26511  rlimcnp2  27024  xrlimcnp  27026  ppiprm  27209  chtprm  27211  prmorcht  27236  rplogsumlem2  27544  dchrisum0re  27572  uhgrspansubgrlem  29322  disjin  32606  xrge0tsmsd  33048  eulerpartgbij  34354  pibt2  37400  eqvreldisj  38596  mhpind  42581  fiinfi  43563  gneispace  44124  ismnushort  44297  elpwinss  44989  restuni3  45058  nel1nelin  45086  disjinfi  45135  inmap  45152  iocopn  45473  icoopn  45478  icomnfinre  45505  uzinico  45513  islpcn  45595  lptre2pt  45596  limcresiooub  45598  limcresioolb  45599  limsupmnflem  45676  limsupresxr  45722  liminfresxr  45723  liminfvalxr  45739  liminf0  45749  icccncfext  45843  stoweidlem39  45995  stoweidlem50  46006  stoweidlem57  46013  fourierdlem32  46095  fourierdlem33  46096  fourierdlem48  46110  fourierdlem49  46111  fourierdlem71  46133  sge0rnre  46320  sge00  46332  sge0tsms  46336  sge0cl  46337  sge0fsum  46343  sge0sup  46347  sge0less  46348  sge0gerp  46351  sge0resplit  46362  sge0split  46365  sge0iunmptlemre  46371  caragendifcl  46470  hoiqssbllem3  46580  hspmbllem2  46583  pimiooltgt  46666  pimdecfgtioc  46671  pimincfltioc  46672  pimdecfgtioo  46673  pimincfltioo  46674  sssmf  46694  smfaddlem1  46719  smfaddlem2  46720  smfadd  46721  mbfpsssmf  46739  smfmul  46751  smfdiv  46753  smfsuplem1  46767  smfliminflem  46786  fmtno4prm  47500  rhmsubcALTVlem3  48127