mpoeq3dva

Description: Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013)

		Ref	Expression
	Hypothesis	mpoeq3dva.1	$⊢ (φ \land x \in A \land y \in B) \to C = D$
	Assertion	mpoeq3dva	$⊢ φ \to (x \in A, y \in B ⟼ C) = (x \in A, y \in B ⟼ D)$

Step	Hyp	Ref	Expression
1		mpoeq3dva.1	$⊢ (φ \land x \in A \land y \in B) \to C = D$
2	1	3expb	$⊢ (φ \land (x \in A \land y \in B)) \to C = D$
3	2	eqeq2d	$⊢ (φ \land (x \in A \land y \in B)) \to (z = C \leftrightarrow z = D)$
4	3	pm5.32da	$⊢ φ \to (((x \in A \land y \in B) \land z = C) \leftrightarrow ((x \in A \land y \in B) \land z = D))$
5	4	oprabbidv	$⊢ φ \to \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = D)\}$
6		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
7		df-mpo	$⊢ (x \in A, y \in B ⟼ D) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = D)\}$
8	5 6 7	3eqtr4g	$⊢ φ \to (x \in A, y \in B ⟼ C) = (x \in A, y \in B ⟼ D)$

Metamath Proof Explorer