Theorem dffun4

Description: Alternate definition of a function. Definition 6.4(4) of TakeutiZaring p. 24. (Contributed by NM, 29-Dec-1996)

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

Proof

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