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

Metamath Proof Explorer

Theorem offveq

Description: Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses offveq.1 ⊢ φ → A ∈ V
offveq.2 ⊢ φ → F Fn A
offveq.3 ⊢ φ → G Fn A
offveq.4 ⊢ φ → H Fn A
offveq.5 ⊢ φ ∧ x ∈ A → F ⁡ x = B
offveq.6 ⊢ φ ∧ x ∈ A → G ⁡ x = C
offveq.7 ⊢ φ ∧ x ∈ A → B R C = H ⁡ x
Assertion offveq ⊢ φ → F R f G = H

Proof

Step Hyp Ref Expression
1 offveq.1 ⊢ φ → A ∈ V
2 offveq.2 ⊢ φ → F Fn A
3 offveq.3 ⊢ φ → G Fn A
4 offveq.4 ⊢ φ → H Fn A
5 offveq.5 ⊢ φ ∧ x ∈ A → F ⁡ x = B
6 offveq.6 ⊢ φ ∧ x ∈ A → G ⁡ x = C
7 offveq.7 ⊢ φ ∧ x ∈ A → B R C = H ⁡ x
8 inidm ⊢ A ∩ A = A
9 2 3 1 1 8 offn ⊢ φ → F R f G Fn A
10 2 3 1 1 8 5 6 ofval ⊢ φ ∧ x ∈ A → F R f G ⁡ x = B R C
11 10 7 eqtrd ⊢ φ ∧ x ∈ A → F R f G ⁡ x = H ⁡ x
12 9 4 11 eqfnfvd ⊢ φ → F R f G = H