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

Metamath Proof Explorer

Theorem cbvsbcvw

Description: Change the bound variable of a class substitution using implicit substitution. Version of cbvsbcv with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 30-Sep-2008) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

		Ref	Expression
	Hypothesis	cbvsbcvw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	Assertion	cbvsbcvw	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑦 ] 𝜓 )

Proof

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