Description: The structure replacement function is a function. (Contributed by SO, 12-Jul-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | fsets | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difss | |
|
2 | fssres | |
|
3 | 1 2 | mpan2 | |
4 | ffn | |
|
5 | fnresdm | |
|
6 | 4 5 | syl | |
7 | 6 | reseq1d | |
8 | resres | |
|
9 | invdif | |
|
10 | 9 | reseq2i | |
11 | 8 10 | eqtri | |
12 | 7 11 | eqtr3di | |
13 | 12 | feq1d | |
14 | 3 13 | mpbird | |
15 | 14 | adantl | |
16 | fsnunf2 | |
|
17 | 15 16 | syl3an1 | |
18 | simp1l | |
|
19 | simp3 | |
|
20 | setsval | |
|
21 | 20 | feq1d | |
22 | 18 19 21 | syl2anc | |
23 | 17 22 | mpbird | |