Theorem csbsng

Description: Distribute proper substitution through the singleton of a class. csbsng is derived from the virtual deduction proof csbsngVD . (Contributed by Alan Sare, 10-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		csbab	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝑦 = 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 }
2		sbceq2g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 ↔ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
3	2	abbidv	⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 = 𝐵 } = { 𝑦 ∣ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )
4	1 3	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝑦 = 𝐵 } = { 𝑦 ∣ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )
5		df-sn	⊢ { 𝐵 } = { 𝑦 ∣ 𝑦 = 𝐵 }
6	5	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝑦 = 𝐵 }
7		df-sn	⊢ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } = { 𝑦 ∣ 𝑦 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
8	4 6 7	3eqtr4g	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )