Metamath Proof Explorer


Theorem iineq1d

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

Ref Expression
Hypothesis iineq1d.1
|- ( ph -> A = B )
Assertion iineq1d
|- ( ph -> |^|_ x e. A C = |^|_ x e. B C )

Proof

Step Hyp Ref Expression
1 iineq1d.1
 |-  ( ph -> A = B )
2 iineq1
 |-  ( A = B -> |^|_ x e. A C = |^|_ x e. B C )
3 1 2 syl
 |-  ( ph -> |^|_ x e. A C = |^|_ x e. B C )