Description: Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was extracted from a former cbvabv version. (Contributed by Wolf Lammen, 16-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cbvsbv.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
Assertion | cbvsbv | |- ( [ z / x ] ph <-> [ z / y ] ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvsbv.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
2 | sbco2vv | |- ( [ z / y ] [ y / x ] ph <-> [ z / x ] ph ) |
|
3 | 1 | sbievw | |- ( [ y / x ] ph <-> ps ) |
4 | 3 | sbbii | |- ( [ z / y ] [ y / x ] ph <-> [ z / y ] ps ) |
5 | 2 4 | bitr3i | |- ( [ z / x ] ph <-> [ z / y ] ps ) |