Theorem fnfvor

Description: Relation between two functions implies the same relation for the function value at a given X . See also fnfvof . (Contributed by Thierry Arnoux, 15-Jan-2026)

	Ref	Expression
Hypotheses	fnfvor.1	$$⊢\phi \to FFnA$$
	fnfvor.2	$$⊢\phi \to GFnA$$
	fnfvor.3	$$⊢\phi \to A\in V$$
	fnfvor.4	$$⊢\phi \to F{R}_{f}G$$
	fnfvor.5	$$⊢\phi \to X\in A$$
Assertion	fnfvor	$$⊢\phi \to F\left(X\right)RG\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnfvor.1	$$⊢\phi \to FFnA$$
2		fnfvor.2	$$⊢\phi \to GFnA$$
3		fnfvor.3	$$⊢\phi \to A\in V$$
4		fnfvor.4	$$⊢\phi \to F{R}_{f}G$$
5		fnfvor.5	$$⊢\phi \to X\in A$$
6		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
7		fveq2	$$⊢x=X\to G\left(x\right)=G\left(X\right)$$
8	6 7	breq12d	$$⊢x=X\to \left(F\left(x\right)RG\left(x\right)\leftrightarrow F\left(X\right)RG\left(X\right)\right)$$
9		inidm	$$⊢A\cap A=A$$
10		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
11		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to G\left(x\right)=G\left(x\right)$$
12	1 2 3 3 9 10 11	ofrfval	$$⊢\phi \to \left(F{R}_{f}G\leftrightarrow \forall x\in AF\left(x\right)RG\left(x\right)\right)$$
13	4 12	mpbid	$$⊢\phi \to \forall x\in AF\left(x\right)RG\left(x\right)$$
14	8 13 5	rspcdva	$$⊢\phi \to F\left(X\right)RG\left(X\right)$$