Theorem ffvbr

Description: Relation with function value. (Contributed by Zhi Wang, 25-Nov-2025)

	Ref	Expression
Assertion	ffvbr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2	1	ffund	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → Fun 𝐹 )
3		simpr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
4	1	fdmd	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → dom 𝐹 = 𝐴 )
5	3 4	eleqtrrd	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ dom 𝐹 )
6		funfvbrb	⊢ ( Fun 𝐹 → ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) ) )
7	6	biimpa	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) )
8	2 5 7	syl2anc	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 𝐹 ( 𝐹 ‘ 𝑋 ) )