Theorem elinel1 4181

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938

This theorem is referenced by:  elin1d  4184  nel1nelin  4187  inss1  4217  predel  6315  fvcofneq  7088  frrlem4  8293  frrlem12  8301  wfrlem4OLD  8331  erdisj  8778  f1opwfi  9373  fival  9429  fi0  9437  dffi2  9440  elfiun  9447  epfrs  9750  r0weon  10031  fodomfi2  10079  ackbij1lem6  10243  ackbij1lem9  10246  ackbij1lem10  10247  ackbij1lem11  10248  fin23lem24  10341  fin23lem26  10344  isfin1-3  10405  canthp1lem2  10672  dedekindle  11404  uzdisj  13619  nn0disj  13666  lo1resb  15585  rlimresb  15586  o1resb  15587  ackbijnn  15849  prmreclem2  16942  isacs2  17670  acsfn  17676  isdrs2  18323  isacs3lem  18557  psssdm2  18596  resscntz  19321  rngcid  20600  ringcid  20629  rhmsubclem3  20652  mplind  22033  clsval2  22993  mreclatdemoBAD  23039  ordtrest  23145  fincmp  23336  discmp  23341  uncmp  23346  ptcnplem  23564  txkgen  23595  infil  23806  hauspwpwf1  23930  alexsubALTlem3  23992  alexsubALTlem4  23993  blbas  24374  blres  24375  xrge0tsms  24779  nmhmcn  25076  ncvsge0  25110  cphsscph  25208  mbfadd  25619  mbfsub  25620  i1fima2  25637  i1fd  25639  mbfmul  25684  bddmulibl  25797  limcun  25853  pilem2  26419  rlimcnp2  26933  xrlimcnp  26935  ppiprm  27118  chtprm  27120  prmorcht  27145  rplogsumlem2  27453  dchrisum0re  27481  uhgrspansubgrlem  29274  disjin  32572  xrge0tsmsd  33061  eulerpartgbij  34409  pibt2  37440  eqvreldisj  38637  mhpind  42592  fiinfi  43572  gneispace  44133  ismnushort  44300  elpwinss  45053  restuni3  45122  disjinfi  45196  inmap  45213  iocopn  45529  icoopn  45534  icomnfinre  45561  uzinico  45568  islpcn  45648  lptre2pt  45649  limcresiooub  45651  limcresioolb  45652  limsupmnflem  45729  limsupresxr  45775  liminfresxr  45776  liminfvalxr  45792  liminf0  45802  icccncfext  45896  stoweidlem39  46048  stoweidlem50  46059  stoweidlem57  46066  fourierdlem32  46148  fourierdlem33  46149  fourierdlem48  46163  fourierdlem49  46164  fourierdlem71  46186  sge0rnre  46373  sge00  46385  sge0tsms  46389  sge0cl  46390  sge0fsum  46396  sge0sup  46400  sge0less  46401  sge0gerp  46404  sge0resplit  46415  sge0split  46418  sge0iunmptlemre  46424  caragendifcl  46523  hoiqssbllem3  46633  hspmbllem2  46636  pimiooltgt  46719  pimdecfgtioc  46724  pimincfltioc  46725  pimdecfgtioo  46726  pimincfltioo  46727  sssmf  46747  smfaddlem1  46772  smfaddlem2  46773  smfadd  46774  mbfpsssmf  46792  smfmul  46804  smfdiv  46806  smfsuplem1  46820  smfliminflem  46839  fmtno4prm  47569  rhmsubcALTVlem3  48238