dffun3

Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996) (Proof shortened by SN, 19-Dec-2024)

		Ref	Expression
	Assertion	dffun3	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \exists z \forall y (x A y \to y = z))$

Step	Hyp	Ref	Expression
1		dffun6	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \exists^{*} y x A y)$
2		dfmo	$⊢ \exists^{*} y x A y \leftrightarrow \exists z \forall y (x A y \to y = z)$
3	2	albii	$⊢ \forall x \exists^{*} y x A y \leftrightarrow \forall x \exists z \forall y (x A y \to y = z)$
4	3	anbi2i	$⊢ (Rel A \land \forall x \exists^{*} y x A y) \leftrightarrow (Rel A \land \forall x \exists z \forall y (x A y \to y = z))$
5	1 4	bitri	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \exists z \forall y (x A y \to y = z))$

Metamath Proof Explorer