Theorem elinel2 4096

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

Syntax hints:   → wi 4   ∈ wcel 2112   ∩ cin 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860

This theorem is referenced by:  elin2d  4099  eldmeldmressn  5880  onfr  6230  partfun  6503  fvcofneq  6890  offres  7734  fsplitfpar  7865  ressuppss  7903  frrlem4  8008  frrlem11  8015  frrlem12  8016  wfrlem4  8036  smores3  8068  erdisj  8421  dffi2  9017  r0weon  9591  fodomfi2  9639  ackbij1lem6  9804  ackbij1lem9  9807  ackbij1lem10  9808  ackbij1lem11  9809  ackbij1lem18  9816  isfin1-3  9965  dedekindle  10961  uzdisj  13150  nn0disj  13193  rlimres  15084  lo1res  15085  ackbijnn  15355  bitsinv2  15965  bitsf1ocnv  15966  smueqlem  16012  prmrec  16438  isstruct2  16676  isacs2  17110  isdrs2  17767  isacs3lem  18002  subrgpropd  19789  sralmod  20178  basdif0  21804  clsval2  21901  mreclatdemoBAD  21947  restfpw  22030  fincmp  22244  discmp  22249  uncmp  22254  cmpfi  22259  bwth  22261  iunconn  22279  1stcrest  22304  infil  22714  alexsublem  22895  alexsubALTlem3  22900  tsmsfbas  22979  tsmsgsum  22990  tsmssubm  22994  tsmsres  22995  tsmsf1o  22996  tsmsmhm  22997  tsmsadd  22998  tsmsxplem1  23004  tsmsxp  23006  blres  23283  reconnlem2  23678  xrge0tsms  23685  ncvsge0  24004  cphsscph  24102  cfilres  24147  ioombl1lem4  24412  mbfadd  24512  mbfsub  24513  mbfmul  24578  itg2cnlem2  24614  bddmulibl  24690  ellimc2  24728  fsumvma2  26049  vmasum  26051  chpchtsum  26054  chebbnd1lem1  26304  dirith2  26363  uhgrspansubgrlem  27332  disjin2  30599  xrge0tsmsd  30990  prsdm  31532  prsrn  31533  pibt2  35274  heicant  35498  mndoisexid  35713  eqvreldisj  36413  fiinfi  40797  ismnushort  41533  restuni3  42281  nel2nelin  42310  disjinfi  42345  inmap  42363  iocopn  42674  icoopn  42679  icomnfinre  42706  uzinico  42714  islpcn  42798  lptre2pt  42799  limcresiooub  42801  limcresioolb  42802  limclner  42810  limsupmnflem  42879  limsupresxr  42925  liminfresxr  42926  liminfvalxr  42942  icccncfext  43046  stoweidlem39  43198  stoweidlem50  43209  stoweidlem57  43216  fourierdlem32  43298  fourierdlem33  43299  fourierdlem48  43313  fourierdlem49  43314  fourierdlem71  43336  fourierdlem80  43345  qndenserrnbllem  43453  sge0rnre  43520  sge0z  43531  sge0tsms  43536  sge0cl  43537  sge0f1o  43538  sge0fsum  43543  sge0sup  43547  sge0rnbnd  43549  sge0ltfirp  43556  sge0resplit  43562  sge0le  43563  sge0split  43565  sge0iunmptlemre  43571  sge0ltfirpmpt2  43582  sge0isum  43583  sge0xaddlem1  43589  sge0xaddlem2  43590  sge0pnffsumgt  43598  sge0gtfsumgt  43599  sge0uzfsumgt  43600  sge0seq  43602  sge0reuz  43603  meadjiunlem  43621  caragendifcl  43670  omeiunltfirp  43675  carageniuncllem2  43678  caratheodorylem2  43683  hspmbllem2  43783  pimiooltgt  43863  pimdecfgtioc  43867  pimincfltioc  43868  pimdecfgtioo  43869  pimincfltioo  43870  sssmf  43889  smfaddlem1  43913  smfaddlem2  43914  smfadd  43915  mbfpsssmf  43933  smfmullem4  43943  smfmul  43944  smfdiv  43946  smfsuplem1  43959  smfliminflem  43978  fmtno4prm  44643  rnghmsubcsetclem2  45150  rhmsubcsetclem2  45196  rhmsubcrngclem2  45202