Description: Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008) (Revised by Mario Carneiro, 13-Oct-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbvcsbv.1 | |- ( x = y -> B = C ) |
|
| Assertion | cbvcsbv | |- [_ A / x ]_ B = [_ A / y ]_ C |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvcsbv.1 | |- ( x = y -> B = C ) |
|
| 2 | nfcv | |- F/_ y B |
|
| 3 | nfcv | |- F/_ x C |
|
| 4 | 2 3 1 | cbvcsbw | |- [_ A / x ]_ B = [_ A / y ]_ C |