Theorem dffun3f

Description: Alternate definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Emmett Weisz, 14-Mar-2021)

	Ref	Expression
Hypotheses	dffun3f.1	|- F/_ x A
	dffun3f.2	|- F/_ y A
	dffun3f.3	|- F/_ z A
Assertion	dffun3f	|- ( Fun A <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )

Proof

Step	Hyp	Ref	Expression
1		dffun3f.1	|- F/_ x A
2		dffun3f.2	|- F/_ y A
3		dffun3f.3	|- F/_ z A
4	1 2	dffun6f	|- ( Fun A <-> ( Rel A /\ A. x E* y x A y ) )
5		nfcv	|- F/_ z x
6		nfcv	|- F/_ z y
7	5 3 6	nfbr	|- F/ z x A y
8	7	mof	|- ( E* y x A y <-> E. z A. y ( x A y -> y = z ) )
9	8	albii	|- ( A. x E* y x A y <-> A. x E. z A. y ( x A y -> y = z ) )
10	9	anbi2i	|- ( ( Rel A /\ A. x E* y x A y ) <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )
11	4 10	bitri	|- ( Fun A <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )