This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) ) )