Metamath Proof Explorer


Theorem ovmpordx

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