Theorem dffun5

Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996)

	Ref	Expression
Assertion	dffun5	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dffun3	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) )
2		df-br	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
3	2	imbi1i	⊢ ( ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) )
4	3	albii	⊢ ( ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ↔ ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) )
5	4	exbii	⊢ ( ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ↔ ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) )
6	5	albii	⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ↔ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) )
7	6	anbi2i	⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) ) )
8	1 7	bitri	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) ) )