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 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cbvsbv ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜓 )

Proof

Step Hyp Ref Expression
1 cbvsbv.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 sbco2vv ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 )
3 1 sbievw ( [ 𝑦 / 𝑥 ] 𝜑𝜓 )
4 3 sbbii ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜓 )
5 2 4 bitr3i ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜓 )