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→FFnA
2 fnafv2elrn ⊢FFnA∧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 imbitrid ⊢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