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 ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∈ dom ⁡ A ∃* y ∈ ran ⁡ A x A y

Proof

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