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

Metamath Proof Explorer

Theorem ovmpodx

Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses ovmpodx.1 ⊢ φ → F = x ∈ C , y ∈ D ⟼ R
ovmpodx.2 ⊢ φ ∧ x = A ∧ y = B → R = S
ovmpodx.3 ⊢ φ ∧ x = A → D = L
ovmpodx.4 ⊢ φ → A ∈ C
ovmpodx.5 ⊢ φ → B ∈ L
ovmpodx.6 ⊢ φ → S ∈ X
Assertion ovmpodx ⊢ φ → A F B = S

Proof

Step Hyp Ref Expression
1 ovmpodx.1 ⊢ φ → F = x ∈ C , y ∈ D ⟼ R
2 ovmpodx.2 ⊢ φ ∧ x = A ∧ y = B → R = S
3 ovmpodx.3 ⊢ φ ∧ x = A → D = L
4 ovmpodx.4 ⊢ φ → A ∈ C
5 ovmpodx.5 ⊢ φ → B ∈ L
6 ovmpodx.6 ⊢ φ → S ∈ X
7 nfv ⊢ Ⅎ x φ
8 nfv ⊢ Ⅎ y φ
9 nfcv ⊢ Ⅎ _ y A
10 nfcv ⊢ Ⅎ _ x B
11 nfcv ⊢ Ⅎ _ x S
12 nfcv ⊢ Ⅎ _ y S
13 1 2 3 4 5 6 7 8 9 10 11 12 ovmpodxf ⊢ φ → A F B = S