Description: Version of setrec2 with a disjoint variable condition instead of a non-freeness hypothesis. (Contributed by Emmett Weisz, 6-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | setrec2.b | |- B = setrecs ( F ) |
|
setrec2.c | |- ( ph -> A. a ( a C_ C -> ( F ` a ) C_ C ) ) |
||
Assertion | setrec2v | |- ( ph -> B C_ C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | setrec2.b | |- B = setrecs ( F ) |
|
2 | setrec2.c | |- ( ph -> A. a ( a C_ C -> ( F ` a ) C_ C ) ) |
|
3 | nfcv | |- F/_ a F |
|
4 | 3 1 2 | setrec2 | |- ( ph -> B C_ C ) |