Theorem csbconstg

Description: Substitution doesn't affect a constant B (in which x does not occur). csbconstgf with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012) Avoid ax-12 . (Revised by Gino Giotto, 15-Oct-2024)

	Ref	Expression
Assertion	csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		csbeq1	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
2	1	eqeq1d	⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
3		df-csb	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 }
4		sbcg	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
5	4	elv	⊢ ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 )
6	5	abbii	⊢ { 𝑧 ∣ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 } = { 𝑧 ∣ 𝑧 ∈ 𝐵 }
7		abid2	⊢ { 𝑧 ∣ 𝑧 ∈ 𝐵 } = 𝐵
8	3 6 7	3eqtri	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵
9	2 8	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 )