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	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) )