Description: Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mpoxopoveq.f | |
|
Assertion | mpoxopoveq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpoxopoveq.f | |
|
2 | 1 | a1i | |
3 | fveq2 | |
|
4 | op1stg | |
|
5 | 4 | adantr | |
6 | 3 5 | sylan9eqr | |
7 | 6 | adantrr | |
8 | sbceq1a | |
|
9 | 8 | adantl | |
10 | 9 | adantl | |
11 | sbceq1a | |
|
12 | 11 | adantr | |
13 | 12 | adantl | |
14 | 10 13 | bitrd | |
15 | 7 14 | rabeqbidv | |
16 | opex | |
|
17 | 16 | a1i | |
18 | simpr | |
|
19 | rabexg | |
|
20 | 19 | ad2antrr | |
21 | equid | |
|
22 | nfvd | |
|
23 | 21 22 | ax-mp | |
24 | nfvd | |
|
25 | 21 24 | ax-mp | |
26 | nfcv | |
|
27 | nfcv | |
|
28 | nfsbc1v | |
|
29 | nfcv | |
|
30 | 28 29 | nfrabw | |
31 | nfsbc1v | |
|
32 | 26 31 | nfsbcw | |
33 | nfcv | |
|
34 | 32 33 | nfrabw | |
35 | 2 15 6 17 18 20 23 25 26 27 30 34 | ovmpodxf | |