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

Metamath Proof Explorer

Theorem ovmpogad

Description: Value of an operation given by a maps-to rule. Deduction form of ovmpoga . (Contributed by SN, 14-Mar-2025)

Ref Expression
Hypotheses ovmpogad.f ⊢ F = x ∈ C , y ∈ D ⟼ R
ovmpogad.s ⊢ x = A ∧ y = B → R = S
ovmpogad.1 ⊢ φ → A ∈ C
ovmpogad.2 ⊢ φ → B ∈ D
ovmpogad.v ⊢ φ → S ∈ V
Assertion ovmpogad ⊢ φ → A F B = S

Proof

Step Hyp Ref Expression
1 ovmpogad.f ⊢ F = x ∈ C , y ∈ D ⟼ R
2 ovmpogad.s ⊢ x = A ∧ y = B → R = S
3 ovmpogad.1 ⊢ φ → A ∈ C
4 ovmpogad.2 ⊢ φ → B ∈ D
5 ovmpogad.v ⊢ φ → S ∈ V
6 1 a1i ⊢ φ → F = x ∈ C , y ∈ D ⟼ R
7 2 adantl ⊢ φ ∧ x = A ∧ y = B → R = S
8 6 7 3 4 5 ovmpod ⊢ φ → A F B = S