mpteq12f

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

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

Step	Hyp	Ref	Expression
1		nfa1	$⊢ Ⅎ x \forall x A = C$
2		nfra1	$⊢ Ⅎ x \forall x \in A B = D$
3	1 2	nfan	$⊢ Ⅎ x (\forall x A = C \land \forall x \in A B = D)$
4		nfv	$⊢ Ⅎ y (\forall x A = C \land \forall x \in A B = D)$
5		rspa	$⊢ (\forall x \in A B = D \land x \in A) \to B = D$
6	5	eqeq2d	$⊢ (\forall x \in A B = D \land x \in A) \to (y = B \leftrightarrow y = D)$
7	6	pm5.32da	$⊢ \forall x \in A B = D \to ((x \in A \land y = B) \leftrightarrow (x \in A \land y = D))$
8		sp	$⊢ \forall x A = C \to A = C$
9	8	eleq2d	$⊢ \forall x A = C \to (x \in A \leftrightarrow x \in C)$
10	9	anbi1d	$⊢ \forall x A = C \to ((x \in A \land y = D) \leftrightarrow (x \in C \land y = D))$
11	7 10	sylan9bbr	$⊢ (\forall x A = C \land \forall x \in A B = D) \to ((x \in A \land y = B) \leftrightarrow (x \in C \land y = D))$
12	3 4 11	opabbid	$⊢ (\forall x A = C \land \forall x \in A B = D) \to \{⟨x, y⟩ \| (x \in A \land y = B)\} = \{⟨x, y⟩ \| (x \in C \land y = D)\}$
13		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
14		df-mpt	$⊢ (x \in C ⟼ D) = \{⟨x, y⟩ \| (x \in C \land y = D)\}$
15	12 13 14	3eqtr4g	$⊢ (\forall x A = C \land \forall x \in A B = D) \to (x \in A ⟼ B) = (x \in C ⟼ D)$

Metamath Proof Explorer