Theorem csbvarg

Description: The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005)

	Ref	Expression
Assertion	csbvarg	$$⊢A\in V\to ⦋A/x⦌x=A$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		df-csb	$$⊢⦋y/x⦌x=\left\{z|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}z\in x\right\}$$
3		sbcel2gv	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}z\in x\leftrightarrow z\in y\right)$$
4	3	abbi1dv	$$⊢y\in \mathrm{V}\to \left\{z|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}z\in x\right\}=y$$
5	2 4	syl5eq	$$⊢y\in \mathrm{V}\to ⦋y/x⦌x=y$$
6	5	elv	$$⊢⦋y/x⦌x=y$$
7	6	csbeq2i	$$⊢⦋A/y⦌⦋y/x⦌x=⦋A/y⦌y$$
8		csbcow	$$⊢⦋A/y⦌⦋y/x⦌x=⦋A/x⦌x$$
9		df-csb	$$⊢⦋A/y⦌y=\left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in y\right\}$$
10	7 8 9	3eqtr3i	$$⊢⦋A/x⦌x=\left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in y\right\}$$
11		sbcel2gv	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in y\leftrightarrow z\in A\right)$$
12	11	abbi1dv	$$⊢A\in \mathrm{V}\to \left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in y\right\}=A$$
13	10 12	syl5eq	$$⊢A\in \mathrm{V}\to ⦋A/x⦌x=A$$
14	1 13	syl	$$⊢A\in V\to ⦋A/x⦌x=A$$