Theorem elinel2 4131

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

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

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895

This theorem is referenced by:  elin2d  4134  eldmeldmressn  5938  onfr  6309  partfun  6589  fvcofneq  6978  offres  7835  fsplitfpar  7968  ressuppss  8008  frrlem4  8114  frrlem11  8121  frrlem12  8122  wfrlem4OLD  8152  smores3  8193  erdisj  8559  dffi2  9191  r0weon  9777  fodomfi2  9825  ackbij1lem6  9990  ackbij1lem9  9993  ackbij1lem10  9994  ackbij1lem11  9995  ackbij1lem18  10002  isfin1-3  10151  dedekindle  11148  uzdisj  13338  nn0disj  13381  rlimres  15276  lo1res  15277  ackbijnn  15549  bitsinv2  16159  bitsf1ocnv  16160  smueqlem  16206  prmrec  16632  isstruct2  16859  isacs2  17371  isdrs2  18033  isacs3lem  18269  subrgpropd  20068  sralmod  20466  basdif0  22112  clsval2  22210  mreclatdemoBAD  22256  restfpw  22339  fincmp  22553  discmp  22558  uncmp  22563  cmpfi  22568  bwth  22570  iunconn  22588  1stcrest  22613  infil  23023  alexsublem  23204  alexsubALTlem3  23209  tsmsfbas  23288  tsmsgsum  23299  tsmssubm  23303  tsmsres  23304  tsmsf1o  23305  tsmsmhm  23306  tsmsadd  23307  tsmsxplem1  23313  tsmsxp  23315  blres  23593  reconnlem2  23999  xrge0tsms  24006  ncvsge0  24326  cphsscph  24424  cfilres  24469  ioombl1lem4  24734  mbfadd  24834  mbfsub  24835  mbfmul  24900  itg2cnlem2  24936  bddmulibl  25012  ellimc2  25050  fsumvma2  26371  vmasum  26373  chpchtsum  26376  chebbnd1lem1  26626  dirith2  26685  uhgrspansubgrlem  27666  disjin2  30935  xrge0tsmsd  31326  prsdm  31873  prsrn  31874  pibt2  35597  heicant  35821  mndoisexid  36036  eqvreldisj  36734  fiinfi  41187  ismnushort  41926  restuni3  42674  nel2nelin  42703  disjinfi  42738  inmap  42756  iocopn  43065  icoopn  43070  icomnfinre  43097  uzinico  43105  islpcn  43187  lptre2pt  43188  limcresiooub  43190  limcresioolb  43191  limclner  43199  limsupmnflem  43268  limsupresxr  43314  liminfresxr  43315  liminfvalxr  43331  icccncfext  43435  stoweidlem39  43587  stoweidlem50  43598  stoweidlem57  43605  fourierdlem32  43687  fourierdlem33  43688  fourierdlem48  43702  fourierdlem49  43703  fourierdlem71  43725  fourierdlem80  43734  qndenserrnbllem  43842  sge0rnre  43909  sge0z  43920  sge0tsms  43925  sge0cl  43926  sge0f1o  43927  sge0fsum  43932  sge0sup  43936  sge0rnbnd  43938  sge0ltfirp  43945  sge0resplit  43951  sge0le  43952  sge0split  43954  sge0iunmptlemre  43960  sge0ltfirpmpt2  43971  sge0isum  43972  sge0xaddlem1  43978  sge0xaddlem2  43979  sge0pnffsumgt  43987  sge0gtfsumgt  43988  sge0uzfsumgt  43989  sge0seq  43991  sge0reuz  43992  meadjiunlem  44010  caragendifcl  44059  omeiunltfirp  44064  carageniuncllem2  44067  caratheodorylem2  44072  hspmbllem2  44172  pimiooltgt  44255  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  sssmf  44283  smfaddlem1  44308  smfaddlem2  44309  smfadd  44310  mbfpsssmf  44328  smfmullem4  44339  smfmul  44340  smfdiv  44342  smfsuplem1  44355  smfliminflem  44374  fmtno4prm  45038  rnghmsubcsetclem2  45545  rhmsubcsetclem2  45591  rhmsubcrngclem2  45597