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

Metamath Proof Explorer

Theorem dffun9

Description: Alternate definition of a function. (Contributed by NM, 28-Mar-2007) (Revised by NM, 16-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 dffun7 ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 brelrn ⊢ ( 𝑥 𝐴 𝑦 → 𝑦 ∈ ran 𝐴 )
5 4 pm4.71ri ⊢ ( 𝑥 𝐴 𝑦 ↔ ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
6 5 mobii ⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃* 𝑦 ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
7 df-rmo ⊢ ( ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 ↔ ∃* 𝑦 ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
8 6 7 bitr4i ⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 )
9 8 ralbii ⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 )
10 9 anbi2i ⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 ) )
11 1 10 bitri ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 ) )