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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  elin2d  4134  nel2nelin  4137  eldmeldmressn  5977  onfr  6349  partfun  6632  fvcofneq  7034  offres  7925  fsplitfpar  8057  ressuppss  8123  frrlem4  8229  frrlem11  8236  frrlem12  8237  smores3  8283  erdisj  8691  dffi2  9326  r0weon  9925  fodomfi2  9973  ackbij1lem6  10137  ackbij1lem9  10140  ackbij1lem10  10141  ackbij1lem11  10142  ackbij1lem18  10149  isfin1-3  10299  dedekindle  11301  uzdisj  13542  nn0disj  13589  rlimres  15511  lo1res  15512  ackbijnn  15784  bitsinv2  16403  bitsf1ocnv  16404  smueqlem  16450  prmrec  16884  isstruct2  17110  isacs2  17610  isdrs2  18263  isacs3lem  18499  subrngpropd  20540  subrgpropd  20580  rnghmsubcsetclem2  20604  rhmsubcsetclem2  20633  rhmsubcrngclem2  20639  sralmod  21177  basdif0  22936  clsval2  23033  mreclatdemoBAD  23079  restfpw  23162  fincmp  23376  discmp  23381  uncmp  23386  cmpfi  23391  bwth  23393  iunconn  23411  1stcrest  23436  infil  23846  alexsublem  24027  alexsubALTlem3  24032  tsmsfbas  24111  tsmsgsum  24122  tsmssubm  24126  tsmsres  24127  tsmsf1o  24128  tsmsmhm  24129  tsmsadd  24130  tsmsxplem1  24136  tsmsxp  24138  blres  24414  reconnlem2  24811  xrge0tsms  24818  ncvsge0  25138  cphsscph  25236  cfilres  25281  ioombl1lem4  25546  mbfadd  25646  mbfsub  25647  mbfmul  25711  itg2cnlem2  25747  bddmulibl  25824  ellimc2  25862  fsumvma2  27195  vmasum  27197  chpchtsum  27200  chebbnd1lem1  27450  dirith2  27509  uhgrspansubgrlem  29377  disjin2  32676  xrge0tsmsd  33154  prsdm  34098  prsrn  34099  pibt2  37779  heicant  38022  mndoisexid  38236  eqvreldisj  39065  eldisjsim2  39302  fiinfi  44017  ismnushort  44745  restuni3  45565  disjinfi  45639  inmap  45654  iocopn  45965  icoopn  45970  icomnfinre  45997  uzinico  46004  islpcn  46082  lptre2pt  46083  limcresiooub  46085  limcresioolb  46086  limclner  46094  limsupmnflem  46163  limsupresxr  46209  liminfresxr  46210  liminfvalxr  46226  icccncfext  46330  stoweidlem39  46482  stoweidlem50  46493  stoweidlem57  46500  fourierdlem32  46582  fourierdlem33  46583  fourierdlem48  46597  fourierdlem49  46598  fourierdlem71  46620  fourierdlem80  46629  qndenserrnbllem  46737  sge0rnre  46807  sge0z  46818  sge0tsms  46823  sge0cl  46824  sge0f1o  46825  sge0fsum  46830  sge0sup  46834  sge0rnbnd  46836  sge0ltfirp  46843  sge0resplit  46849  sge0le  46850  sge0split  46852  sge0iunmptlemre  46858  sge0ltfirpmpt2  46869  sge0isum  46870  sge0xaddlem1  46876  sge0xaddlem2  46877  sge0pnffsumgt  46885  sge0gtfsumgt  46886  sge0uzfsumgt  46887  sge0seq  46889  sge0reuz  46890  meadjiunlem  46908  caragendifcl  46957  omeiunltfirp  46962  carageniuncllem2  46965  caratheodorylem2  46970  hspmbllem2  47070  pimiooltgt  47153  pimdecfgtioc  47158  pimincfltioc  47159  pimdecfgtioo  47160  pimincfltioo  47161  sssmf  47181  smfaddlem1  47206  smfaddlem2  47207  smfadd  47208  mbfpsssmf  47226  smfmullem4  47237  smfmul  47238  smfdiv  47240  smfsuplem1  47254  smfliminflem  47273  fmtno4prm  48053