Theorem elinel2 4195

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3954

This theorem is referenced by:  elin2d  4198  eldmeldmressn  6023  onfr  6400  partfun  6694  fvcofneq  7090  offres  7965  fsplitfpar  8099  ressuppss  8163  frrlem4  8269  frrlem11  8276  frrlem12  8277  wfrlem4OLD  8307  smores3  8348  erdisj  8751  dffi2  9414  r0weon  10003  fodomfi2  10051  ackbij1lem6  10216  ackbij1lem9  10219  ackbij1lem10  10220  ackbij1lem11  10221  ackbij1lem18  10228  isfin1-3  10377  dedekindle  11374  uzdisj  13570  nn0disj  13613  rlimres  15498  lo1res  15499  ackbijnn  15770  bitsinv2  16380  bitsf1ocnv  16381  smueqlem  16427  prmrec  16851  isstruct2  17078  isacs2  17593  isdrs2  18255  isacs3lem  18491  subrgpropd  20388  sralmod  20796  basdif0  22438  clsval2  22536  mreclatdemoBAD  22582  restfpw  22665  fincmp  22879  discmp  22884  uncmp  22889  cmpfi  22894  bwth  22896  iunconn  22914  1stcrest  22939  infil  23349  alexsublem  23530  alexsubALTlem3  23535  tsmsfbas  23614  tsmsgsum  23625  tsmssubm  23629  tsmsres  23630  tsmsf1o  23631  tsmsmhm  23632  tsmsadd  23633  tsmsxplem1  23639  tsmsxp  23641  blres  23919  reconnlem2  24325  xrge0tsms  24332  ncvsge0  24652  cphsscph  24750  cfilres  24795  ioombl1lem4  25060  mbfadd  25160  mbfsub  25161  mbfmul  25226  itg2cnlem2  25262  bddmulibl  25338  ellimc2  25376  fsumvma2  26697  vmasum  26699  chpchtsum  26702  chebbnd1lem1  26952  dirith2  27011  uhgrspansubgrlem  28527  disjin2  31796  xrge0tsmsd  32187  prsdm  32832  prsrn  32833  pibt2  36236  heicant  36461  mndoisexid  36675  eqvreldisj  37422  fiinfi  42257  ismnushort  42993  restuni3  43740  nel2nelin  43769  disjinfi  43824  inmap  43841  iocopn  44168  icoopn  44173  icomnfinre  44200  uzinico  44208  islpcn  44290  lptre2pt  44291  limcresiooub  44293  limcresioolb  44294  limclner  44302  limsupmnflem  44371  limsupresxr  44417  liminfresxr  44418  liminfvalxr  44434  icccncfext  44538  stoweidlem39  44690  stoweidlem50  44701  stoweidlem57  44708  fourierdlem32  44790  fourierdlem33  44791  fourierdlem48  44805  fourierdlem49  44806  fourierdlem71  44828  fourierdlem80  44837  qndenserrnbllem  44945  sge0rnre  45015  sge0z  45026  sge0tsms  45031  sge0cl  45032  sge0f1o  45033  sge0fsum  45038  sge0sup  45042  sge0rnbnd  45044  sge0ltfirp  45051  sge0resplit  45057  sge0le  45058  sge0split  45060  sge0iunmptlemre  45066  sge0ltfirpmpt2  45077  sge0isum  45078  sge0xaddlem1  45084  sge0xaddlem2  45085  sge0pnffsumgt  45093  sge0gtfsumgt  45094  sge0uzfsumgt  45095  sge0seq  45097  sge0reuz  45098  meadjiunlem  45116  caragendifcl  45165  omeiunltfirp  45170  carageniuncllem2  45173  caratheodorylem2  45178  hspmbllem2  45278  pimiooltgt  45361  pimdecfgtioc  45366  pimincfltioc  45367  pimdecfgtioo  45368  pimincfltioo  45369  sssmf  45389  smfaddlem1  45414  smfaddlem2  45415  smfadd  45416  mbfpsssmf  45434  smfmullem4  45445  smfmul  45446  smfdiv  45448  smfsuplem1  45462  smfliminflem  45481  fmtno4prm  46178  subrngpropd  46680  rnghmsubcsetclem2  46776  rhmsubcsetclem2  46822  rhmsubcrngclem2  46828