ffvbr

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

		Ref	Expression
	Assertion	ffvbr	$⊢ (F : A ⟶ B \land X \in A) \to X F F (X)$

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

Metamath Proof Explorer