Metamath Proof Explorer

Theorem fafv2elrnb

Description: An alternate function value is defined, i.e., belongs to the range of the function, iff its argument is in the domain of the function. (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion fafv2elrnb ⊢ F : A ⟶ B → C ∈ A ↔ F '''' C ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 ffn ⊢ F : A ⟶ B → F Fn A
2 fnafv2elrn ⊢ F Fn A ∧ C ∈ A → F '''' C ∈ ran ⁡ F
3 1 2 sylan ⊢ F : A ⟶ B ∧ C ∈ A → F '''' C ∈ ran ⁡ F
4 3 ex ⊢ F : A ⟶ B → C ∈ A → F '''' C ∈ ran ⁡ F
5 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
6 ndmafv2nrn ⊢ ¬ C ∈ dom ⁡ F → F '''' C ∉ ran ⁡ F
7 df-nel ⊢ F '''' C ∉ ran ⁡ F ↔ ¬ F '''' C ∈ ran ⁡ F
8 6 7 sylib ⊢ ¬ C ∈ dom ⁡ F → ¬ F '''' C ∈ ran ⁡ F
9 8 con4i ⊢ F '''' C ∈ ran ⁡ F → C ∈ dom ⁡ F
10 eleq2 ⊢ dom ⁡ F = A → C ∈ dom ⁡ F ↔ C ∈ A
11 9 10 syl5ib ⊢ dom ⁡ F = A → F '''' C ∈ ran ⁡ F → C ∈ A
12 5 11 syl ⊢ F : A ⟶ B → F '''' C ∈ ran ⁡ F → C ∈ A
13 4 12 impbid ⊢ F : A ⟶ B → C ∈ A ↔ F '''' C ∈ ran ⁡ F