Description: Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | f1stres | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | |
|
2 | vex | |
|
3 | 1 2 | op1sta | |
4 | 3 | eleq1i | |
5 | 4 | biimpri | |
6 | 5 | adantr | |
7 | 6 | rgen2 | |
8 | sneq | |
|
9 | 8 | dmeqd | |
10 | 9 | unieqd | |
11 | 10 | eleq1d | |
12 | 11 | ralxp | |
13 | 7 12 | mpbir | |
14 | df-1st | |
|
15 | 14 | reseq1i | |
16 | ssv | |
|
17 | resmpt | |
|
18 | 16 17 | ax-mp | |
19 | 15 18 | eqtri | |
20 | 19 | fmpt | |
21 | 13 20 | mpbi | |