Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005) (Revised by Mario Carneiro, 11-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rspc.1 | |
|
rspc.2 | |
||
Assertion | rspc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspc.1 | |
|
2 | rspc.2 | |
|
3 | df-ral | |
|
4 | nfcv | |
|
5 | nfv | |
|
6 | 5 1 | nfim | |
7 | eleq1 | |
|
8 | 7 2 | imbi12d | |
9 | 4 6 8 | spcgf | |
10 | 9 | pm2.43a | |
11 | 3 10 | syl5bi | |