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

Metamath Proof Explorer

Theorem dffun8

Description: Alternate definition of a function. One possibility for the definition of a function in Enderton p. 42. Compare dffun7 . (Contributed by NM, 4-Nov-2002) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion dffun8 ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃! 𝑦 𝑥 𝐴 𝑦 ) )

Proof

Step Hyp Ref Expression
1 dffun7 ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
2 moeu ⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑦 𝑥 𝐴 𝑦 → ∃! 𝑦 𝑥 𝐴 𝑦 ) )
3 vex ⊢ 𝑥 ∈ V
4 3 eldm ⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 𝑥 𝐴 𝑦 )
5 pm5.5 ⊢ ( ∃ 𝑦 𝑥 𝐴 𝑦 → ( ( ∃ 𝑦 𝑥 𝐴 𝑦 → ∃! 𝑦 𝑥 𝐴 𝑦 ) ↔ ∃! 𝑦 𝑥 𝐴 𝑦 ) )
6 4 5 sylbi ⊢ ( 𝑥 ∈ dom 𝐴 → ( ( ∃ 𝑦 𝑥 𝐴 𝑦 → ∃! 𝑦 𝑥 𝐴 𝑦 ) ↔ ∃! 𝑦 𝑥 𝐴 𝑦 ) )
7 2 6 bitrid ⊢ ( 𝑥 ∈ dom 𝐴 → ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃! 𝑦 𝑥 𝐴 𝑦 ) )
8 7 ralbiia ⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ∈ dom 𝐴 ∃! 𝑦 𝑥 𝐴 𝑦 )
9 8 anbi2i ⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃! 𝑦 𝑥 𝐴 𝑦 ) )
10 1 9 bitri ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃! 𝑦 𝑥 𝐴 𝑦 ) )