Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | csbiegf.1 | |
|
csbiegf.2 | |
||
Assertion | csbiegf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbiegf.1 | |
|
2 | csbiegf.2 | |
|
3 | 2 | ax-gen | |
4 | csbiebt | |
|
5 | 1 4 | mpdan | |
6 | 3 5 | mpbii | |