Metamath Proof Explorer


Theorem iineq1d

Description: Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypothesis iineq1d.1 ( 𝜑𝐴 = 𝐵 )
Assertion iineq1d ( 𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 iineq1d.1 ( 𝜑𝐴 = 𝐵 )
2 iineq1 ( 𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶 )
3 1 2 syl ( 𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶 )