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	$$⊢A\in V\to ⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		csbab	$$⊢⦋A/x⦌\left\{y|y=B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}$$
2		sbceq2g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow y=⦋A/x⦌B\right)$$
3	2	abbidv	$$⊢A\in V\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}$$
4	1 3	eqtrid	$$⊢A\in V\to ⦋A/x⦌\left\{y|y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}$$
5		df-sn	$$⊢\left\{B\right\}=\left\{y|y=B\right\}$$
6	5	csbeq2i	$$⊢⦋A/x⦌\left\{B\right\}=⦋A/x⦌\left\{y|y=B\right\}$$
7		df-sn	$$⊢\left\{⦋A/x⦌B\right\}=\left\{y|y=⦋A/x⦌B\right\}$$
8	4 6 7	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}$$