Description: Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rspcimdv.1 | |
|
rspcimdv.2 | |
||
Assertion | rspcimdv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspcimdv.1 | |
|
2 | rspcimdv.2 | |
|
3 | df-ral | |
|
4 | simpr | |
|
5 | 4 | eleq1d | |
6 | 5 | biimprd | |
7 | 6 2 | imim12d | |
8 | 1 7 | spcimdv | |
9 | 1 8 | mpid | |
10 | 3 9 | syl5bi | |