Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Basic algebraic structures (extension)
Auxiliary theorems
ovmpordx
Metamath Proof Explorer
Description: Value of an operation given by a maps-to rule, deduction form, with
substitution of second argument, analogous to ovmpodxf . (Contributed by AV , 30-Mar-2019)
Ref
Expression
Hypotheses
ovmpordx.1
⊢ φ → F = x ∈ C , y ∈ D ⟼ R
ovmpordx.2
⊢ φ ∧ x = A ∧ y = B → R = S
ovmpordx.3
⊢ φ ∧ y = B → C = L
ovmpordx.4
⊢ φ → A ∈ L
ovmpordx.5
⊢ φ → B ∈ D
ovmpordx.6
⊢ φ → S ∈ X
Assertion
ovmpordx
⊢ φ → A F B = S
Proof
Step
Hyp
Ref
Expression
1
ovmpordx.1
⊢ φ → F = x ∈ C , y ∈ D ⟼ R
2
ovmpordx.2
⊢ φ ∧ x = A ∧ y = B → R = S
3
ovmpordx.3
⊢ φ ∧ y = B → C = L
4
ovmpordx.4
⊢ φ → A ∈ L
5
ovmpordx.5
⊢ φ → B ∈ D
6
ovmpordx.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
ovmpordxf
⊢ φ → A F B = S