Theorem 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 <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )

Proof

Step	Hyp	Ref	Expression
1		dffun6	|- ( Fun A <-> ( Rel A /\ A. x E* y x A y ) )
2		df-mo	|- ( E* y x A y <-> E. z A. y ( x A y -> y = z ) )
3	2	albii	|- ( A. x E* y x A y <-> A. x E. z A. y ( x A y -> y = z ) )
4	3	anbi2i	|- ( ( Rel A /\ A. x E* y x A y ) <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )
5	1 4	bitri	|- ( Fun A <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )