| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-csb |
|- [_ y / x ]_ B = { z | [. y / x ]. z e. B } |
| 2 |
1
|
eqabri |
|- ( z e. [_ y / x ]_ B <-> [. y / x ]. z e. B ) |
| 3 |
2
|
sbcbii |
|- ( [. A / y ]. z e. [_ y / x ]_ B <-> [. A / y ]. [. y / x ]. z e. B ) |
| 4 |
|
sbccow |
|- ( [. A / y ]. [. y / x ]. z e. B <-> [. A / x ]. z e. B ) |
| 5 |
3 4
|
bitri |
|- ( [. A / y ]. z e. [_ y / x ]_ B <-> [. A / x ]. z e. B ) |
| 6 |
5
|
abbii |
|- { z | [. A / y ]. z e. [_ y / x ]_ B } = { z | [. A / x ]. z e. B } |
| 7 |
|
df-csb |
|- [_ A / y ]_ [_ y / x ]_ B = { z | [. A / y ]. z e. [_ y / x ]_ B } |
| 8 |
|
df-csb |
|- [_ A / x ]_ B = { z | [. A / x ]. z e. B } |
| 9 |
6 7 8
|
3eqtr4i |
|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B |