Theorem bj-csbsn

Description: Substitution in a singleton. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-csbsn	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 } = { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		bj-csbsnlem	⊢ ⦋ 𝑦 / 𝑥 ⦌ { 𝑥 } = { 𝑦 }
2	1	csbeq2i	⊢ ⦋ 𝐴 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ { 𝑥 } = ⦋ 𝐴 / 𝑦 ⦌ { 𝑦 }
3		csbcow	⊢ ⦋ 𝐴 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ { 𝑥 } = ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 }
4		bj-csbsnlem	⊢ ⦋ 𝐴 / 𝑦 ⦌ { 𝑦 } = { 𝐴 }
5	2 3 4	3eqtr3i	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 } = { 𝐴 }