This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iineq1

Description: Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998)

		Ref	Expression
	Assertion	iineq1	$⊢ A = B \to ⋂_{x \in A} C = ⋂_{x \in B} C$

Step	Hyp	Ref	Expression
1		raleq	$⊢ A = B \to (\forall x \in A y \in C \leftrightarrow \forall x \in B y \in C)$
2	1	abbidv	$⊢ A = B \to \{y \| \forall x \in A y \in C\} = \{y \| \forall x \in B y \in C\}$
3		df-iin	$⊢ ⋂_{x \in A} C = \{y \| \forall x \in A y \in C\}$
4		df-iin	$⊢ ⋂_{x \in B} C = \{y \| \forall x \in B y \in C\}$
5	2 3 4	3eqtr4g	$⊢ A = B \to ⋂_{x \in A} C = ⋂_{x \in B} C$