Theorem cbvsbcvw2

Description: Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw . (Contributed by GG, 1-Sep-2025)

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

Proof

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