Theorem dffun7

Description: Alternate definition of a function. One possibility for the definition of a function in Enderton p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one". However, dffun8 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002)

	Ref	Expression
Assertion	dffun7	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		dffun6	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
2		moabs	⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑦 𝑥 𝐴 𝑦 → ∃* 𝑦 𝑥 𝐴 𝑦 ) )
3		vex	⊢ 𝑥 ∈ V
4	3	eldm	⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 𝑥 𝐴 𝑦 )
5	4	imbi1i	⊢ ( ( 𝑥 ∈ dom 𝐴 → ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( ∃ 𝑦 𝑥 𝐴 𝑦 → ∃* 𝑦 𝑥 𝐴 𝑦 ) )
6	2 5	bitr4i	⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ( 𝑥 ∈ dom 𝐴 → ∃* 𝑦 𝑥 𝐴 𝑦 ) )
7	6	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ dom 𝐴 → ∃* 𝑦 𝑥 𝐴 𝑦 ) )
8		df-ral	⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ dom 𝐴 → ∃* 𝑦 𝑥 𝐴 𝑦 ) )
9	7 8	bitr4i	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 )
10	9	anbi2i	⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
11	1 10	bitri	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) )