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

Metamath Proof Explorer

Theorem cbvsbc

Description: Change bound variables in a wff substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvsbcw when possible. (Contributed by Jeff Hankins, 19-Sep-2009) (Proof shortened by Andrew Salmon, 8-Jun-2011) (New usage is discouraged.)

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

Proof

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