mpov

Description: Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013)

		Ref	Expression
	Assertion	mpov	$⊢ (x \in V, y \in V ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| z = C\}$

Step	Hyp	Ref	Expression
1		df-mpo	$⊢ (x \in V, y \in V ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in V \land y \in V) \land z = C)\}$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	pm3.2i	$⊢ (x \in V \land y \in V)$
5	4	biantrur	$⊢ z = C \leftrightarrow ((x \in V \land y \in V) \land z = C)$
6	5	oprabbii	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = C\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in V \land y \in V) \land z = C)\}$
7	1 6	eqtr4i	$⊢ (x \in V, y \in V ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| z = C\}$

Metamath Proof Explorer