Theorem csb2

Description: Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that x can be free in B but cannot occur in A . (Contributed by NM, 2-Dec-2013)

	Ref	Expression
Assertion	csb2	$$⊢⦋A/x⦌B=\left\{y|\exists x\left(x=A\wedge y\in B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
2		sbc5	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow \exists x\left(x=A\wedge y\in B\right)$$
3	2	abbii	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\left\{y|\exists x\left(x=A\wedge y\in B\right)\right\}$$
4	1 3	eqtri	$$⊢⦋A/x⦌B=\left\{y|\exists x\left(x=A\wedge y\in B\right)\right\}$$