Theorem ffvbr

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

	Ref	Expression
Assertion	ffvbr	$$⊢\left(F:A⟶B\wedge X\in A\right)\to XFF\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(F:A⟶B\wedge X\in A\right)\to F:A⟶B$$
2	1	ffund	$$⊢\left(F:A⟶B\wedge X\in A\right)\to \mathrm{Fun}F$$
3		simpr	$$⊢\left(F:A⟶B\wedge X\in A\right)\to X\in A$$
4	1	fdmd	$$⊢\left(F:A⟶B\wedge X\in A\right)\to \mathrm{dom}F=A$$
5	3 4	eleqtrrd	$$⊢\left(F:A⟶B\wedge X\in A\right)\to X\in \mathrm{dom}F$$
6		funfvbrb	$$⊢\mathrm{Fun}F\to \left(X\in \mathrm{dom}F\leftrightarrow XFF\left(X\right)\right)$$
7	6	biimpa	$$⊢\left(\mathrm{Fun}F\wedge X\in \mathrm{dom}F\right)\to XFF\left(X\right)$$
8	2 5 7	syl2anc	$$⊢\left(F:A⟶B\wedge X\in A\right)\to XFF\left(X\right)$$