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 | |- ( ph -> F = ( x e. C , y e. D |-> R ) ) |
|
| ovmpordx.2 | |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S ) |
||
| ovmpordx.3 | |- ( ( ph /\ y = B ) -> C = L ) |
||
| ovmpordx.4 | |- ( ph -> A e. L ) |
||
| ovmpordx.5 | |- ( ph -> B e. D ) |
||
| ovmpordx.6 | |- ( ph -> S e. X ) |
||
| Assertion | ovmpordx | |- ( ph -> ( A F B ) = S ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ovmpordx.1 | |- ( ph -> F = ( x e. C , y e. D |-> R ) ) |
|
| 2 | ovmpordx.2 | |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S ) |
|
| 3 | ovmpordx.3 | |- ( ( ph /\ y = B ) -> C = L ) |
|
| 4 | ovmpordx.4 | |- ( ph -> A e. L ) |
|
| 5 | ovmpordx.5 | |- ( ph -> B e. D ) |
|
| 6 | ovmpordx.6 | |- ( ph -> S e. X ) |
|
| 7 | nfv | |- F/ x ph |
|
| 8 | nfv | |- F/ y ph |
|
| 9 | nfcv | |- F/_ y A |
|
| 10 | nfcv | |- F/_ x B |
|
| 11 | nfcv | |- F/_ x S |
|
| 12 | nfcv | |- F/_ y S |
|
| 13 | 1 2 3 4 5 6 7 8 9 10 11 12 | ovmpordxf | |- ( ph -> ( A F B ) = S ) |