Theorem dffun6f

Description: Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	dffun6f.1	|- F/_ x A
	dffun6f.2	|- F/_ y A
Assertion	dffun6f	|- ( Fun A <-> ( Rel A /\ A. x E* y x A y ) )

Proof

Step	Hyp	Ref	Expression
1		dffun6f.1	|- F/_ x A
2		dffun6f.2	|- F/_ y A
3		dffun3	|- ( Fun A <-> ( Rel A /\ A. w E. u A. v ( w A v -> v = u ) ) )
4		nfcv	|- F/_ y w
5		nfcv	|- F/_ y v
6	4 2 5	nfbr	|- F/ y w A v
7		nfv	|- F/ v w A y
8		breq2	|- ( v = y -> ( w A v <-> w A y ) )
9	6 7 8	cbvmow	|- ( E* v w A v <-> E* y w A y )
10	9	albii	|- ( A. w E* v w A v <-> A. w E* y w A y )
11		df-mo	|- ( E* v w A v <-> E. u A. v ( w A v -> v = u ) )
12	11	albii	|- ( A. w E* v w A v <-> A. w E. u A. v ( w A v -> v = u ) )
13		nfcv	|- F/_ x w
14		nfcv	|- F/_ x y
15	13 1 14	nfbr	|- F/ x w A y
16	15	nfmov	|- F/ x E* y w A y
17		nfv	|- F/ w E* y x A y
18		breq1	|- ( w = x -> ( w A y <-> x A y ) )
19	18	mobidv	|- ( w = x -> ( E* y w A y <-> E* y x A y ) )
20	16 17 19	cbvalv1	|- ( A. w E* y w A y <-> A. x E* y x A y )
21	10 12 20	3bitr3ri	|- ( A. x E* y x A y <-> A. w E. u A. v ( w A v -> v = u ) )
22	21	anbi2i	|- ( ( Rel A /\ A. x E* y x A y ) <-> ( Rel A /\ A. w E. u A. v ( w A v -> v = u ) ) )
23	3 22	bitr4i	|- ( Fun A <-> ( Rel A /\ A. x E* y x A y ) )