Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014) (Revised by Mario Carneiro, 13-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | csbied.1 | |- ( ph -> A e. V ) |
|
csbied.2 | |- ( ( ph /\ x = A ) -> B = C ) |
||
Assertion | csbied | |- ( ph -> [_ A / x ]_ B = C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbied.1 | |- ( ph -> A e. V ) |
|
2 | csbied.2 | |- ( ( ph /\ x = A ) -> B = C ) |
|
3 | nfv | |- F/ x ph |
|
4 | nfcvd | |- ( ph -> F/_ x C ) |
|
5 | 3 4 1 2 | csbiedf | |- ( ph -> [_ A / x ]_ B = C ) |