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

Metamath Proof Explorer

Theorem inteq

Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999)

		Ref	Expression
	Assertion	inteq	$⊢ A = B \to ⋂ A = ⋂ B$

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