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	⊢ Ⅎ 𝑥 𝐴
	dffun3f.2	⊢ Ⅎ 𝑦 𝐴
	dffun3f.3	⊢ Ⅎ 𝑧 𝐴
Assertion	dffun3f	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dffun3f.1	⊢ Ⅎ 𝑥 𝐴
2		dffun3f.2	⊢ Ⅎ 𝑦 𝐴
3		dffun3f.3	⊢ Ⅎ 𝑧 𝐴
4	1 2	dffun6f	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
5		nfcv	⊢ Ⅎ 𝑧 𝑥
6		nfcv	⊢ Ⅎ 𝑧 𝑦
7	5 3 6	nfbr	⊢ Ⅎ 𝑧 𝑥 𝐴 𝑦
8	7	mof	⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) )
9	8	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) )
10	9	anbi2i	⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) )
11	4 10	bitri	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) )