Description: Function analogue of subid . (Contributed by Steve Rodriguez, 5-Nov-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ofsubid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | ffn | |
|
3 | 2 | adantl | |
4 | c0ex | |
|
5 | 4 | fconst | |
6 | ffn | |
|
7 | 5 6 | mp1i | |
8 | eqidd | |
|
9 | ffvelcdm | |
|
10 | 9 | subidd | |
11 | 10 | adantll | |
12 | 4 | fvconst2 | |
13 | 12 | adantl | |
14 | 11 13 | eqtr4d | |
15 | 1 3 3 7 8 8 14 | offveq | |