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 )