MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iineq2dv Structured version   Visualization version   GIF version

Theorem iineq2dv 4695
Description: Equality deduction for indexed intersection. (Contributed by NM, 3-Aug-2004.)
Hypothesis
Ref Expression
iuneq2dv.1 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
Assertion
Ref Expression
iineq2dv (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iineq2dv
StepHypRef Expression
1 nfv 1992 . 2 𝑥𝜑
2 iuneq2dv.1 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
31, 2iineq2d 4693 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2139   ciin 4673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ral 3055  df-iin 4675
This theorem is referenced by:  cntziinsn  17987  ptbasfi  21606  fclsval  22033  taylfval  24332  polfvalN  35711  dihglblem3N  37104  dihmeetlem2N  37108  iineq12dv  39806  saliincl  41066  iccvonmbllem  41416  vonicclem2  41422  smflimlem3  41505  smflimlem4  41506  smflimlem6  41508  smflimsuplem3  41552
  Copyright terms: Public domain W3C validator