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

Theorem iineq2dv 4925
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 1916 . 2 𝑥𝜑
2 iuneq2dv.1 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
31, 2iineq2d 4923 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2115   ciin 4901
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3137  df-iin 4903
This theorem is referenced by:  cntziinsn  18454  ptbasfi  22175  fclsval  22602  taylfval  24943  polfvalN  37100  dihglblem3N  38491  dihmeetlem2N  38495  iineq12dv  41580  saliincl  42809  iccvonmbllem  43159  vonicclem2  43165  smflimlem3  43248  smflimlem4  43249  smflimlem6  43251  smflimsuplem3  43295
  Copyright terms: Public domain W3C validator