mpoeq123dva

Description: An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017)

Step	Hyp	Ref	Expression
1		mpoeq123dv.1	$⊢ φ \to A = D$
2		mpoeq123dva.2	$⊢ (φ \land x \in A) \to B = E$
3		mpoeq123dva.3	$⊢ (φ \land (x \in A \land y \in B)) \to C = F$
4	3	eqeq2d	$⊢ (φ \land (x \in A \land y \in B)) \to (z = C \leftrightarrow z = F)$
5	4	pm5.32da	$⊢ φ \to (((x \in A \land y \in B) \land z = C) \leftrightarrow ((x \in A \land y \in B) \land z = F))$
6	2	eleq2d	$⊢ (φ \land x \in A) \to (y \in B \leftrightarrow y \in E)$
7	6	pm5.32da	$⊢ φ \to ((x \in A \land y \in B) \leftrightarrow (x \in A \land y \in E))$
8	1	eleq2d	$⊢ φ \to (x \in A \leftrightarrow x \in D)$
9	8	anbi1d	$⊢ φ \to ((x \in A \land y \in E) \leftrightarrow (x \in D \land y \in E))$
10	7 9	bitrd	$⊢ φ \to ((x \in A \land y \in B) \leftrightarrow (x \in D \land y \in E))$
11	10	anbi1d	$⊢ φ \to (((x \in A \land y \in B) \land z = F) \leftrightarrow ((x \in D \land y \in E) \land z = F))$
12	5 11	bitrd	$⊢ φ \to (((x \in A \land y \in B) \land z = C) \leftrightarrow ((x \in D \land y \in E) \land z = F))$
13	12	oprabbidv	$⊢ φ \to \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in D \land y \in E) \land z = F)\}$
14		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
15		df-mpo	$⊢ (x \in D, y \in E ⟼ F) = \{⟨⟨x, y⟩, z⟩ \| ((x \in D \land y \in E) \land z = F)\}$
16	13 14 15	3eqtr4g	$⊢ φ \to (x \in A, y \in B ⟼ C) = (x \in D, y \in E ⟼ F)$

Metamath Proof Explorer