This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )