Description: A version of rspcev using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rspcegf.1 | |
|
rspcegf.2 | |
||
rspcegf.3 | |
||
rspcegf.4 | |
||
Assertion | rspcegf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspcegf.1 | |
|
2 | rspcegf.2 | |
|
3 | rspcegf.3 | |
|
4 | rspcegf.4 | |
|
5 | 2 3 | nfel | |
6 | 5 1 | nfan | |
7 | eleq1 | |
|
8 | 7 4 | anbi12d | |
9 | 2 6 8 | spcegf | |
10 | 9 | anabsi5 | |
11 | df-rex | |
|
12 | 10 11 | sylibr | |