funopab

Description: A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995)

		Ref	Expression
	Assertion	funopab	$⊢ Fun \{⟨x, y⟩ \| φ\} \leftrightarrow \forall x \exists^{*} y φ$

Step	Hyp	Ref	Expression
1		relopabv	$⊢ Rel \{⟨x, y⟩ \| φ\}$
2		nfopab1	$⊢ \underline{Ⅎ} x \{⟨x, y⟩ \| φ\}$
3		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| φ\}$
4	2 3	dffun6f	$⊢ Fun \{⟨x, y⟩ \| φ\} \leftrightarrow (Rel \{⟨x, y⟩ \| φ\} \land \forall x \exists^{*} y x \{⟨x, y⟩ \| φ\} y)$
5	1 4	mpbiran	$⊢ Fun \{⟨x, y⟩ \| φ\} \leftrightarrow \forall x \exists^{*} y x \{⟨x, y⟩ \| φ\} y$
6		df-br	$⊢ x \{⟨x, y⟩ \| φ\} y \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\}$
7		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow φ$
8	6 7	bitri	$⊢ x \{⟨x, y⟩ \| φ\} y \leftrightarrow φ$
9	8	mobii	$⊢ \exists^{} y x \{⟨x, y⟩ \| φ\} y \leftrightarrow \exists^{} y φ$
10	9	albii	$⊢ \forall x \exists^{} y x \{⟨x, y⟩ \| φ\} y \leftrightarrow \forall x \exists^{} y φ$
11	5 10	bitri	$⊢ Fun \{⟨x, y⟩ \| φ\} \leftrightarrow \forall x \exists^{*} y φ$

Metamath Proof Explorer