Theorem bj-csbsn

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

	Ref	Expression
Assertion	bj-csbsn	$$⊢⦋A/x⦌\left\{x\right\}=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		bj-csbsnlem	$$⊢⦋y/x⦌\left\{x\right\}=\left\{y\right\}$$
2	1	csbeq2i	$$⊢⦋A/y⦌⦋y/x⦌\left\{x\right\}=⦋A/y⦌\left\{y\right\}$$
3		csbcow	$$⊢⦋A/y⦌⦋y/x⦌\left\{x\right\}=⦋A/x⦌\left\{x\right\}$$
4		bj-csbsnlem	$$⊢⦋A/y⦌\left\{y\right\}=\left\{A\right\}$$
5	2 3 4	3eqtr3i	$$⊢⦋A/x⦌\left\{x\right\}=\left\{A\right\}$$