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	|- ( ph -> F Fn A )
	fnfvor.2	|- ( ph -> G Fn A )
	fnfvor.3	|- ( ph -> A e. V )
	fnfvor.4	|- ( ph -> F oR R G )
	fnfvor.5	|- ( ph -> X e. A )
Assertion	fnfvor	|- ( ph -> ( F ` X ) R ( G ` X ) )

Proof

Step	Hyp	Ref	Expression
1		fnfvor.1	|- ( ph -> F Fn A )
2		fnfvor.2	|- ( ph -> G Fn A )
3		fnfvor.3	|- ( ph -> A e. V )
4		fnfvor.4	|- ( ph -> F oR R G )
5		fnfvor.5	|- ( ph -> X e. A )
6		fveq2	|- ( x = X -> ( F ` x ) = ( F ` X ) )
7		fveq2	|- ( x = X -> ( G ` x ) = ( G ` X ) )
8	6 7	breq12d	|- ( x = X -> ( ( F ` x ) R ( G ` x ) <-> ( F ` X ) R ( G ` X ) ) )
9		inidm	|- ( A i^i A ) = A
10		eqidd	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
11		eqidd	|- ( ( ph /\ x e. A ) -> ( G ` x ) = ( G ` x ) )
12	1 2 3 3 9 10 11	ofrfval	|- ( ph -> ( F oR R G <-> A. x e. A ( F ` x ) R ( G ` x ) ) )
13	4 12	mpbid	|- ( ph -> A. x e. A ( F ` x ) R ( G ` x ) )
14	8 13 5	rspcdva	|- ( ph -> ( F ` X ) R ( G ` X ) )