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 e. V -> [_ A / x ]_ x = A )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. V -> A e. _V )
2		df-csb	|- [_ y / x ]_ x = { z | [. y / x ]. z e. x }
3		sbcel2gv	|- ( y e. _V -> ( [. y / x ]. z e. x <-> z e. y ) )
4	3	eqabcdv	|- ( y e. _V -> { z | [. y / x ]. z e. x } = y )
5	2 4	eqtrid	|- ( y e. _V -> [_ 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 = { z | [. A / y ]. z e. y }
10	7 8 9	3eqtr3i	|- [_ A / x ]_ x = { z | [. A / y ]. z e. y }
11		sbcel2gv	|- ( A e. _V -> ( [. A / y ]. z e. y <-> z e. A ) )
12	11	eqabcdv	|- ( A e. _V -> { z | [. A / y ]. z e. y } = A )
13	10 12	eqtrid	|- ( A e. _V -> [_ A / x ]_ x = A )
14	1 13	syl	|- ( A e. V -> [_ A / x ]_ x = A )