Metamath Proof Explorer

Theorem dffun3OLD

Description: Obsolete version of dffun3 as of 19-Dec-2024. Alternate definition of function. (Contributed by NM, 29-Dec-1996) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dffun2	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \forall y \forall z ((x A y \land x A z) \to y = z))$
2		breq2	$⊢ y = z \to (x A y \leftrightarrow x A z)$
3	2	mo4	$⊢ \exists^{*} y x A y \leftrightarrow \forall y \forall z ((x A y \land x A z) \to y = z)$
4		df-mo	$⊢ \exists^{*} y x A y \leftrightarrow \exists z \forall y (x A y \to y = z)$
5	3 4	bitr3i	$⊢ \forall y \forall z ((x A y \land x A z) \to y = z) \leftrightarrow \exists z \forall y (x A y \to y = z)$
6	5	albii	$⊢ \forall x \forall y \forall z ((x A y \land x A z) \to y = z) \leftrightarrow \forall x \exists z \forall y (x A y \to y = z)$
7	6	anbi2i	$⊢ (Rel A \land \forall x \forall y \forall z ((x A y \land x A z) \to y = z)) \leftrightarrow (Rel A \land \forall x \exists z \forall y (x A y \to y = z))$
8	1 7	bitri	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \exists z \forall y (x A y \to y = z))$