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	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐶 ∈ 𝐴 ↔ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2		fnafv2elrn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
3	1 2	sylan	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
4	3	ex	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐶 ∈ 𝐴 → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) )
5		fdm	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
6		ndmafv2nrn	⊢ ( ¬ 𝐶 ∈ dom 𝐹 → ( 𝐹 '''' 𝐶 ) ∉ ran 𝐹 )
7		df-nel	⊢ ( ( 𝐹 '''' 𝐶 ) ∉ ran 𝐹 ↔ ¬ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
8	6 7	sylib	⊢ ( ¬ 𝐶 ∈ dom 𝐹 → ¬ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
9	8	con4i	⊢ ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 → 𝐶 ∈ dom 𝐹 )
10		eleq2	⊢ ( dom 𝐹 = 𝐴 → ( 𝐶 ∈ dom 𝐹 ↔ 𝐶 ∈ 𝐴 ) )
11	9 10	imbitrid	⊢ ( dom 𝐹 = 𝐴 → ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 → 𝐶 ∈ 𝐴 ) )
12	5 11	syl	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 → 𝐶 ∈ 𝐴 ) )
13	4 12	impbid	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐶 ∈ 𝐴 ↔ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) )