Theorem iineq2dv 4955

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

Step	Hyp	Ref	Expression
1		nfv 1914	. 2 ⊢ Ⅎ𝑥𝜑
2		iuneq2dv.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	iineq2d 4953	1 ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1538   ∈ wcel 2103  ∩ ciin 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-12 2168  ax-ext 2706

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1779  df-nf 1783  df-sb 2065  df-clab 2713  df-cleq 2727  df-clel 2813  df-ral 3061  df-iin 4933

This theorem is referenced by:  cntziinsn  19000  ptbasfi  22795  fclsval  23222  taylfval  25581  polfvalN  38128  dihglblem3N  39519  dihmeetlem2N  39523  iineq12dv  42882  saliincl  44108  iccvonmbllem  44459  vonicclem2  44465  smflimlem3  44554  smflimlem4  44555  smflimlem6  44557  smflimsuplem3  44603