Theorem elinel2 4191

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
elinel2	⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Proof of Theorem elinel2

Step	Hyp	Ref	Expression
1		elin 3959	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simprbi 496	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2098   ∩ cin 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-v 3470  df-in 3950

This theorem is referenced by:  elin2d  4194  eldmeldmressn  6018  onfr  6396  partfun  6690  fvcofneq  7087  offres  7966  fsplitfpar  8101  ressuppss  8165  frrlem4  8272  frrlem11  8279  frrlem12  8280  wfrlem4OLD  8310  smores3  8351  erdisj  8754  dffi2  9417  r0weon  10006  fodomfi2  10054  ackbij1lem6  10219  ackbij1lem9  10222  ackbij1lem10  10223  ackbij1lem11  10224  ackbij1lem18  10231  isfin1-3  10380  dedekindle  11379  uzdisj  13577  nn0disj  13620  rlimres  15505  lo1res  15506  ackbijnn  15777  bitsinv2  16388  bitsf1ocnv  16389  smueqlem  16435  prmrec  16861  isstruct2  17088  isacs2  17603  isdrs2  18268  isacs3lem  18504  subrngpropd  20465  subrgpropd  20507  rnghmsubcsetclem2  20525  rhmsubcsetclem2  20554  rhmsubcrngclem2  20560  sralmod  21040  basdif0  22806  clsval2  22904  mreclatdemoBAD  22950  restfpw  23033  fincmp  23247  discmp  23252  uncmp  23257  cmpfi  23262  bwth  23264  iunconn  23282  1stcrest  23307  infil  23717  alexsublem  23898  alexsubALTlem3  23903  tsmsfbas  23982  tsmsgsum  23993  tsmssubm  23997  tsmsres  23998  tsmsf1o  23999  tsmsmhm  24000  tsmsadd  24001  tsmsxplem1  24007  tsmsxp  24009  blres  24287  reconnlem2  24693  xrge0tsms  24700  ncvsge0  25031  cphsscph  25129  cfilres  25174  ioombl1lem4  25440  mbfadd  25540  mbfsub  25541  mbfmul  25606  itg2cnlem2  25642  bddmulibl  25718  ellimc2  25756  fsumvma2  27097  vmasum  27099  chpchtsum  27102  chebbnd1lem1  27352  dirith2  27411  uhgrspansubgrlem  29050  disjin2  32322  xrge0tsmsd  32712  prsdm  33423  prsrn  33424  pibt2  36804  heicant  37035  mndoisexid  37249  eqvreldisj  37996  fiinfi  42882  ismnushort  43618  restuni3  44364  nel2nelin  44393  disjinfi  44445  inmap  44462  iocopn  44787  icoopn  44792  icomnfinre  44819  uzinico  44827  islpcn  44909  lptre2pt  44910  limcresiooub  44912  limcresioolb  44913  limclner  44921  limsupmnflem  44990  limsupresxr  45036  liminfresxr  45037  liminfvalxr  45053  icccncfext  45157  stoweidlem39  45309  stoweidlem50  45320  stoweidlem57  45327  fourierdlem32  45409  fourierdlem33  45410  fourierdlem48  45424  fourierdlem49  45425  fourierdlem71  45447  fourierdlem80  45456  qndenserrnbllem  45564  sge0rnre  45634  sge0z  45645  sge0tsms  45650  sge0cl  45651  sge0f1o  45652  sge0fsum  45657  sge0sup  45661  sge0rnbnd  45663  sge0ltfirp  45670  sge0resplit  45676  sge0le  45677  sge0split  45679  sge0iunmptlemre  45685  sge0ltfirpmpt2  45696  sge0isum  45697  sge0xaddlem1  45703  sge0xaddlem2  45704  sge0pnffsumgt  45712  sge0gtfsumgt  45713  sge0uzfsumgt  45714  sge0seq  45716  sge0reuz  45717  meadjiunlem  45735  caragendifcl  45784  omeiunltfirp  45789  carageniuncllem2  45792  caratheodorylem2  45797  hspmbllem2  45897  pimiooltgt  45980  pimdecfgtioc  45985  pimincfltioc  45986  pimdecfgtioo  45987  pimincfltioo  45988  sssmf  46008  smfaddlem1  46033  smfaddlem2  46034  smfadd  46035  mbfpsssmf  46053  smfmullem4  46064  smfmul  46065  smfdiv  46067  smfsuplem1  46081  smfliminflem  46100  fmtno4prm  46797