Description: Lemma for setrec2 . The functional part of F has the same values as F . (Contributed by Emmett Weisz, 4-Mar-2021) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | setrec2lem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvres | |
|
2 | nfvres | |
|
3 | vex | |
|
4 | breq1 | |
|
5 | 4 | eubidv | |
6 | 3 5 | elab | |
7 | tz6.12-2 | |
|
8 | 6 7 | sylnbi | |
9 | 2 8 | eqtr4d | |
10 | 1 9 | pm2.61i | |