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

Metamath Proof Explorer

Theorem funopabeq

Description: A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995)

		Ref	Expression
	Assertion	funopabeq	$⊢ Fun \{⟨x, y⟩ \| y = A\}$

Step	Hyp	Ref	Expression
1		funopab	$⊢ Fun \{⟨x, y⟩ \| y = A\} \leftrightarrow \forall x \exists^{*} y y = A$
2		moeq	$⊢ \exists^{*} y y = A$
3	1 2	mpgbir	$⊢ Fun \{⟨x, y⟩ \| y = A\}$