Metamath Proof Explorer

Theorem dffun6

Description: Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024)

		Ref	Expression
	Assertion	dffun6	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \exists^{*} y x F y)$

Proof

Step	Hyp	Ref	Expression
1		dffun2	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \forall y \forall z ((x F y \land x F z) \to y = z))$
2		breq2	$⊢ y = z \to (x F y \leftrightarrow x F z)$
3	2	mo4	$⊢ \exists^{*} y x F y \leftrightarrow \forall y \forall z ((x F y \land x F z) \to y = z)$
4	3	albii	$⊢ \forall x \exists^{*} y x F y \leftrightarrow \forall x \forall y \forall z ((x F y \land x F z) \to y = z)$
5	4	anbi2i	$⊢ (Rel F \land \forall x \exists^{*} y x F y) \leftrightarrow (Rel F \land \forall x \forall y \forall z ((x F y \land x F z) \to y = z))$
6	1 5	bitr4i	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \exists^{*} y x F y)$