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

Metamath Proof Explorer

Theorem ofreq

Description: Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Assertion ofreq ( 𝑅 = 𝑆 → ∘r 𝑅 = ∘r 𝑆 )

Proof

Step Hyp Ref Expression
1 breq ⊢ ( 𝑅 = 𝑆 → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) ) )
2 1 ralbidv ⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) ) )
3 2 opabbidv ⊢ ( 𝑅 = 𝑆 → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) } )
4 df-ofr ⊢ ∘r 𝑅 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) }
5 df-ofr ⊢ ∘r 𝑆 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) }
6 3 4 5 3eqtr4g ⊢ ( 𝑅 = 𝑆 → ∘r 𝑅 = ∘r 𝑆 )