Theorem elinel2 4202

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958

This theorem is referenced by:  elin2d  4205  nel2nelin  4208  eldmeldmressn  6043  onfr  6423  partfun  6715  fvcofneq  7113  offres  8008  fsplitfpar  8143  ressuppss  8208  frrlem4  8314  frrlem11  8321  frrlem12  8322  wfrlem4OLD  8352  smores3  8393  erdisj  8799  dffi2  9463  r0weon  10052  fodomfi2  10100  ackbij1lem6  10264  ackbij1lem9  10267  ackbij1lem10  10268  ackbij1lem11  10269  ackbij1lem18  10276  isfin1-3  10426  dedekindle  11425  uzdisj  13637  nn0disj  13684  rlimres  15594  lo1res  15595  ackbijnn  15864  bitsinv2  16480  bitsf1ocnv  16481  smueqlem  16527  prmrec  16960  isstruct2  17186  isacs2  17696  isdrs2  18352  isacs3lem  18587  subrngpropd  20568  subrgpropd  20608  rnghmsubcsetclem2  20632  rhmsubcsetclem2  20661  rhmsubcrngclem2  20667  sralmod  21194  basdif0  22960  clsval2  23058  mreclatdemoBAD  23104  restfpw  23187  fincmp  23401  discmp  23406  uncmp  23411  cmpfi  23416  bwth  23418  iunconn  23436  1stcrest  23461  infil  23871  alexsublem  24052  alexsubALTlem3  24057  tsmsfbas  24136  tsmsgsum  24147  tsmssubm  24151  tsmsres  24152  tsmsf1o  24153  tsmsmhm  24154  tsmsadd  24155  tsmsxplem1  24161  tsmsxp  24163  blres  24441  reconnlem2  24849  xrge0tsms  24856  ncvsge0  25187  cphsscph  25285  cfilres  25330  ioombl1lem4  25596  mbfadd  25696  mbfsub  25697  mbfmul  25761  itg2cnlem2  25797  bddmulibl  25874  ellimc2  25912  fsumvma2  27258  vmasum  27260  chpchtsum  27263  chebbnd1lem1  27513  dirith2  27572  uhgrspansubgrlem  29307  disjin2  32600  xrge0tsmsd  33065  prsdm  33913  prsrn  33914  pibt2  37418  heicant  37662  mndoisexid  37876  eqvreldisj  38615  fiinfi  43586  ismnushort  44320  restuni3  45123  disjinfi  45197  inmap  45214  iocopn  45533  icoopn  45538  icomnfinre  45565  uzinico  45573  islpcn  45654  lptre2pt  45655  limcresiooub  45657  limcresioolb  45658  limclner  45666  limsupmnflem  45735  limsupresxr  45781  liminfresxr  45782  liminfvalxr  45798  icccncfext  45902  stoweidlem39  46054  stoweidlem50  46065  stoweidlem57  46072  fourierdlem32  46154  fourierdlem33  46155  fourierdlem48  46169  fourierdlem49  46170  fourierdlem71  46192  fourierdlem80  46201  qndenserrnbllem  46309  sge0rnre  46379  sge0z  46390  sge0tsms  46395  sge0cl  46396  sge0f1o  46397  sge0fsum  46402  sge0sup  46406  sge0rnbnd  46408  sge0ltfirp  46415  sge0resplit  46421  sge0le  46422  sge0split  46424  sge0iunmptlemre  46430  sge0ltfirpmpt2  46441  sge0isum  46442  sge0xaddlem1  46448  sge0xaddlem2  46449  sge0pnffsumgt  46457  sge0gtfsumgt  46458  sge0uzfsumgt  46459  sge0seq  46461  sge0reuz  46462  meadjiunlem  46480  caragendifcl  46529  omeiunltfirp  46534  carageniuncllem2  46537  caratheodorylem2  46542  hspmbllem2  46642  pimiooltgt  46725  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  sssmf  46753  smfaddlem1  46778  smfaddlem2  46779  smfadd  46780  mbfpsssmf  46798  smfmullem4  46809  smfmul  46810  smfdiv  46812  smfsuplem1  46826  smfliminflem  46845  fmtno4prm  47562