Theorem elinel2 4126

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  elin2d  4129  eldmeldmressn  5924  onfr  6290  partfun  6564  fvcofneq  6951  offres  7799  fsplitfpar  7930  ressuppss  7970  frrlem4  8076  frrlem11  8083  frrlem12  8084  wfrlem4OLD  8114  smores3  8155  erdisj  8508  dffi2  9112  r0weon  9699  fodomfi2  9747  ackbij1lem6  9912  ackbij1lem9  9915  ackbij1lem10  9916  ackbij1lem11  9917  ackbij1lem18  9924  isfin1-3  10073  dedekindle  11069  uzdisj  13258  nn0disj  13301  rlimres  15195  lo1res  15196  ackbijnn  15468  bitsinv2  16078  bitsf1ocnv  16079  smueqlem  16125  prmrec  16551  isstruct2  16778  isacs2  17279  isdrs2  17939  isacs3lem  18175  subrgpropd  19974  sralmod  20370  basdif0  22011  clsval2  22109  mreclatdemoBAD  22155  restfpw  22238  fincmp  22452  discmp  22457  uncmp  22462  cmpfi  22467  bwth  22469  iunconn  22487  1stcrest  22512  infil  22922  alexsublem  23103  alexsubALTlem3  23108  tsmsfbas  23187  tsmsgsum  23198  tsmssubm  23202  tsmsres  23203  tsmsf1o  23204  tsmsmhm  23205  tsmsadd  23206  tsmsxplem1  23212  tsmsxp  23214  blres  23492  reconnlem2  23896  xrge0tsms  23903  ncvsge0  24222  cphsscph  24320  cfilres  24365  ioombl1lem4  24630  mbfadd  24730  mbfsub  24731  mbfmul  24796  itg2cnlem2  24832  bddmulibl  24908  ellimc2  24946  fsumvma2  26267  vmasum  26269  chpchtsum  26272  chebbnd1lem1  26522  dirith2  26581  uhgrspansubgrlem  27560  disjin2  30827  xrge0tsmsd  31219  prsdm  31766  prsrn  31767  pibt2  35515  heicant  35739  mndoisexid  35954  eqvreldisj  36654  fiinfi  41069  ismnushort  41808  restuni3  42556  nel2nelin  42585  disjinfi  42620  inmap  42638  iocopn  42948  icoopn  42953  icomnfinre  42980  uzinico  42988  islpcn  43070  lptre2pt  43071  limcresiooub  43073  limcresioolb  43074  limclner  43082  limsupmnflem  43151  limsupresxr  43197  liminfresxr  43198  liminfvalxr  43214  icccncfext  43318  stoweidlem39  43470  stoweidlem50  43481  stoweidlem57  43488  fourierdlem32  43570  fourierdlem33  43571  fourierdlem48  43585  fourierdlem49  43586  fourierdlem71  43608  fourierdlem80  43617  qndenserrnbllem  43725  sge0rnre  43792  sge0z  43803  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0fsum  43815  sge0sup  43819  sge0rnbnd  43821  sge0ltfirp  43828  sge0resplit  43834  sge0le  43835  sge0split  43837  sge0iunmptlemre  43843  sge0ltfirpmpt2  43854  sge0isum  43855  sge0xaddlem1  43861  sge0xaddlem2  43862  sge0pnffsumgt  43870  sge0gtfsumgt  43871  sge0uzfsumgt  43872  sge0seq  43874  sge0reuz  43875  meadjiunlem  43893  caragendifcl  43942  omeiunltfirp  43947  carageniuncllem2  43950  caratheodorylem2  43955  hspmbllem2  44055  pimiooltgt  44135  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  sssmf  44161  smfaddlem1  44185  smfaddlem2  44186  smfadd  44187  mbfpsssmf  44205  smfmullem4  44215  smfmul  44216  smfdiv  44218  smfsuplem1  44231  smfliminflem  44250  fmtno4prm  44915  rnghmsubcsetclem2  45422  rhmsubcsetclem2  45468  rhmsubcrngclem2  45474