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

Metamath Proof Explorer

Theorem mpteq12

Description: An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013)

		Ref	Expression
	Assertion	mpteq12	$⊢ (A = C \land \forall x \in A B = D) \to (x \in A ⟼ B) = (x \in C ⟼ D)$

Step	Hyp	Ref	Expression
1		ax-5	$⊢ A = C \to \forall x A = C$
2		mpteq12f	$⊢ (\forall x A = C \land \forall x \in A B = D) \to (x \in A ⟼ B) = (x \in C ⟼ D)$
3	1 2	sylan	$⊢ (A = C \land \forall x \in A B = D) \to (x \in A ⟼ B) = (x \in C ⟼ D)$