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	⊢ Ⅎ 𝑥 𝐴
	dffun6f.2	⊢ Ⅎ 𝑦 𝐴
Assertion	dffun6f	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		dffun6f.1	⊢ Ⅎ 𝑥 𝐴
2		dffun6f.2	⊢ Ⅎ 𝑦 𝐴
3		dffun3	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑤 ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) ) )
4		nfcv	⊢ Ⅎ 𝑦 𝑤
5		nfcv	⊢ Ⅎ 𝑦 𝑣
6	4 2 5	nfbr	⊢ Ⅎ 𝑦 𝑤 𝐴 𝑣
7		nfv	⊢ Ⅎ 𝑣 𝑤 𝐴 𝑦
8		breq2	⊢ ( 𝑣 = 𝑦 → ( 𝑤 𝐴 𝑣 ↔ 𝑤 𝐴 𝑦 ) )
9	6 7 8	cbvmow	⊢ ( ∃* 𝑣 𝑤 𝐴 𝑣 ↔ ∃* 𝑦 𝑤 𝐴 𝑦 )
10	9	albii	⊢ ( ∀ 𝑤 ∃* 𝑣 𝑤 𝐴 𝑣 ↔ ∀ 𝑤 ∃* 𝑦 𝑤 𝐴 𝑦 )
11		df-mo	⊢ ( ∃* 𝑣 𝑤 𝐴 𝑣 ↔ ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) )
12	11	albii	⊢ ( ∀ 𝑤 ∃* 𝑣 𝑤 𝐴 𝑣 ↔ ∀ 𝑤 ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) )
13		nfcv	⊢ Ⅎ 𝑥 𝑤
14		nfcv	⊢ Ⅎ 𝑥 𝑦
15	13 1 14	nfbr	⊢ Ⅎ 𝑥 𝑤 𝐴 𝑦
16	15	nfmov	⊢ Ⅎ 𝑥 ∃* 𝑦 𝑤 𝐴 𝑦
17		nfv	⊢ Ⅎ 𝑤 ∃* 𝑦 𝑥 𝐴 𝑦
18		breq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝐴 𝑦 ↔ 𝑥 𝐴 𝑦 ) )
19	18	mobidv	⊢ ( 𝑤 = 𝑥 → ( ∃* 𝑦 𝑤 𝐴 𝑦 ↔ ∃* 𝑦 𝑥 𝐴 𝑦 ) )
20	16 17 19	cbvalv1	⊢ ( ∀ 𝑤 ∃* 𝑦 𝑤 𝐴 𝑦 ↔ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 )
21	10 12 20	3bitr3ri	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑤 ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) )
22	21	anbi2i	⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑤 ∃ 𝑢 ∀ 𝑣 ( 𝑤 𝐴 𝑣 → 𝑣 = 𝑢 ) ) )
23	3 22	bitr4i	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )