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

Metamath Proof Explorer

Theorem cbvsbcw

Description: Change bound variables in a wff substitution. Version of cbvsbc with a disjoint variable condition, which does not require ax-13 . (Contributed by Jeff Hankins, 19-Sep-2009) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

	Ref	Expression
Hypotheses	cbvsbcw.1	⊢ Ⅎ 𝑦 𝜑
	cbvsbcw.2	⊢ Ⅎ 𝑥 𝜓
	cbvsbcw.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvsbcw	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑦 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbvsbcw.1	⊢ Ⅎ 𝑦 𝜑
2		cbvsbcw.2	⊢ Ⅎ 𝑥 𝜓
3		cbvsbcw.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4	1 2 3	cbvabw	⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 }
5	4	eleq2i	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑦 ∣ 𝜓 } )
6		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
7		df-sbc	⊢ ( [ 𝐴 / 𝑦 ] 𝜓 ↔ 𝐴 ∈ { 𝑦 ∣ 𝜓 } )
8	5 6 7	3bitr4i	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑦 ] 𝜓 )