This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \to (φ \leftrightarrow ψ)$
	Assertion	cbvsbv	$⊢ [z/ x] φ \leftrightarrow [z/ y] ψ$

Proof

Step	Hyp	Ref	Expression
1		cbvsbv.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		sbco2vv	$⊢ [z/ y] [y/ x] φ \leftrightarrow [z/ x] φ$
3	1	sbievw	$⊢ [y/ x] φ \leftrightarrow ψ$
4	3	sbbii	$⊢ [z/ y] [y/ x] φ \leftrightarrow [z/ y] ψ$
5	2 4	bitr3i	$⊢ [z/ x] φ \leftrightarrow [z/ y] ψ$