Theorem elinel1 4148

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  elin1d  4151  nel1nelin  4154  inss1  4184  predel  6268  fvcofneq  7026  frrlem4  8219  frrlem12  8227  erdisj  8679  f1opwfi  9240  fival  9296  fi0  9304  dffi2  9307  elfiun  9314  epfrs  9621  r0weon  9903  fodomfi2  9951  ackbij1lem6  10115  ackbij1lem9  10118  ackbij1lem10  10119  ackbij1lem11  10120  fin23lem24  10213  fin23lem26  10216  isfin1-3  10277  canthp1lem2  10544  dedekindle  11277  uzdisj  13497  nn0disj  13544  lo1resb  15471  rlimresb  15472  o1resb  15473  ackbijnn  15735  prmreclem2  16829  isacs2  17559  acsfn  17565  isdrs2  18212  isacs3lem  18448  psssdm2  18487  resscntz  19245  rngcid  20550  ringcid  20579  rhmsubclem3  20602  mplind  22005  clsval2  22965  mreclatdemoBAD  23011  ordtrest  23117  fincmp  23308  discmp  23313  uncmp  23318  ptcnplem  23536  txkgen  23567  infil  23778  hauspwpwf1  23902  alexsubALTlem3  23964  alexsubALTlem4  23965  blbas  24345  blres  24346  xrge0tsms  24750  nmhmcn  25047  ncvsge0  25080  cphsscph  25178  mbfadd  25589  mbfsub  25590  i1fima2  25607  i1fd  25609  mbfmul  25654  bddmulibl  25767  limcun  25823  pilem2  26389  rlimcnp2  26903  xrlimcnp  26905  ppiprm  27088  chtprm  27090  prmorcht  27115  rplogsumlem2  27423  dchrisum0re  27451  uhgrspansubgrlem  29268  disjin  32566  xrge0tsmsd  33042  eulerpartgbij  34385  pibt2  37461  dfadjliftmap2  38481  dfblockliftmap2  38484  eqvreldisj  38720  mhpind  42697  fiinfi  43676  gneispace  44237  ismnushort  44404  elpwinss  45156  restuni3  45225  disjinfi  45299  inmap  45316  iocopn  45630  icoopn  45635  icomnfinre  45662  uzinico  45669  islpcn  45747  lptre2pt  45748  limcresiooub  45750  limcresioolb  45751  limsupmnflem  45828  limsupresxr  45874  liminfresxr  45875  liminfvalxr  45891  liminf0  45901  icccncfext  45995  stoweidlem39  46147  stoweidlem50  46158  stoweidlem57  46165  fourierdlem32  46247  fourierdlem33  46248  fourierdlem48  46262  fourierdlem49  46263  fourierdlem71  46285  sge0rnre  46472  sge00  46484  sge0tsms  46488  sge0cl  46489  sge0fsum  46495  sge0sup  46499  sge0less  46500  sge0gerp  46503  sge0resplit  46514  sge0split  46517  sge0iunmptlemre  46523  caragendifcl  46622  hoiqssbllem3  46732  hspmbllem2  46735  pimiooltgt  46818  pimdecfgtioc  46823  pimincfltioc  46824  pimdecfgtioo  46825  pimincfltioo  46826  sssmf  46846  smfaddlem1  46871  smfaddlem2  46872  smfadd  46873  mbfpsssmf  46891  smfmul  46903  smfdiv  46905  smfsuplem1  46919  smfliminflem  46938  nthrucw  46994  fmtno4prm  47685  rhmsubcALTVlem3  48393