Theorem csbeq1

Description: Analogue of dfsbcq for proper substitution into a class. (Contributed by NM, 10-Nov-2005)

	Ref	Expression
Assertion	csbeq1	⊢ ( 𝐴 = 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑥 ⦌ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		dfsbcq	⊢ ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ [ 𝐵 / 𝑥 ] 𝑦 ∈ 𝐶 ) )
2	1	abbidv	⊢ ( 𝐴 = 𝐵 → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } = { 𝑦 ∣ [ 𝐵 / 𝑥 ] 𝑦 ∈ 𝐶 } )
3		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 }
4		df-csb	⊢ ⦋ 𝐵 / 𝑥 ⦌ 𝐶 = { 𝑦 ∣ [ 𝐵 / 𝑥 ] 𝑦 ∈ 𝐶 }
5	2 3 4	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑥 ⦌ 𝐶 )