Theorem ffvbr

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

	Ref	Expression
Assertion	ffvbr	|- ( ( F : A --> B /\ X e. A ) -> X F ( F ` X ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( F : A --> B /\ X e. A ) -> F : A --> B )
2	1	ffund	|- ( ( F : A --> B /\ X e. A ) -> Fun F )
3		simpr	|- ( ( F : A --> B /\ X e. A ) -> X e. A )
4	1	fdmd	|- ( ( F : A --> B /\ X e. A ) -> dom F = A )
5	3 4	eleqtrrd	|- ( ( F : A --> B /\ X e. A ) -> X e. dom F )
6		funfvbrb	|- ( Fun F -> ( X e. dom F <-> X F ( F ` X ) ) )
7	6	biimpa	|- ( ( Fun F /\ X e. dom F ) -> X F ( F ` X ) )
8	2 5 7	syl2anc	|- ( ( F : A --> B /\ X e. A ) -> X F ( F ` X ) )