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 ⊢ φ → F Fn A
fnfvor.2 ⊢ φ → G Fn A
fnfvor.3 ⊢ φ → A ∈ V
fnfvor.4 ⊢ φ → F R f G
fnfvor.5 ⊢ φ → X ∈ A
Assertion fnfvor ⊢ φ → F ⁡ X R G ⁡ X

Proof

Step Hyp Ref Expression
1 fnfvor.1 ⊢ φ → F Fn A
2 fnfvor.2 ⊢ φ → G Fn A
3 fnfvor.3 ⊢ φ → A ∈ V
4 fnfvor.4 ⊢ φ → F R f G
5 fnfvor.5 ⊢ φ → X ∈ 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 ∩ A = A
10 eqidd ⊢ φ ∧ x ∈ A → F ⁡ x = F ⁡ x
11 eqidd ⊢ φ ∧ x ∈ A → G ⁡ x = G ⁡ x
12 1 2 3 3 9 10 11 ofrfval ⊢ φ → F R f G ↔ ∀ x ∈ A F ⁡ x R G ⁡ x
13 4 12 mpbid ⊢ φ → ∀ x ∈ A F ⁡ x R G ⁡ x
14 8 13 5 rspcdva ⊢ φ → F ⁡ X R G ⁡ X