This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )