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

Metamath Proof Explorer

Theorem mptv

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

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

Step	Hyp	Ref	Expression
1		df-mpt	$⊢ (x \in V ⟼ B) = \{⟨x, y⟩ \| (x \in V \land y = B)\}$
2		vex	$⊢ x \in V$
3	2	biantrur	$⊢ y = B \leftrightarrow (x \in V \land y = B)$
4	3	opabbii	$⊢ \{⟨x, y⟩ \| y = B\} = \{⟨x, y⟩ \| (x \in V \land y = B)\}$
5	1 4	eqtr4i	$⊢ (x \in V ⟼ B) = \{⟨x, y⟩ \| y = B\}$