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 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
fnfvor.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
fnfvor.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fnfvor.4 ⊢ ( 𝜑 → 𝐹 ∘r 𝑅 𝐺 )
fnfvor.5 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion fnfvor ( 𝜑 → ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fnfvor.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 fnfvor.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
3 fnfvor.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 fnfvor.4 ⊢ ( 𝜑 → 𝐹 ∘r 𝑅 𝐺 )
5 fnfvor.5 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
6 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
7 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
8 6 7 breq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) )
9 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
10 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
11 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
12 1 2 3 3 9 10 11 ofrfval ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
13 4 12 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) )
14 8 13 5 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) )