Metamath Proof Explorer


Theorem cbvsbv

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 )

Proof

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 )