Theorem csbeq1

Description: Analogue of dfsbcq for proper substitution into a class. (Contributed by NM, 10-Nov-2005)

	Ref	Expression
Assertion	csbeq1	|- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )

Proof

Step	Hyp	Ref	Expression
1		dfsbcq	|- ( A = B -> ( [. A / x ]. y e. C <-> [. B / x ]. y e. C ) )
2	1	abbidv	|- ( A = B -> { y | [. A / x ]. y e. C } = { y | [. B / x ]. y e. C } )
3		df-csb	|- [_ A / x ]_ C = { y | [. A / x ]. y e. C }
4		df-csb	|- [_ B / x ]_ C = { y | [. B / x ]. y e. C }
5	2 3 4	3eqtr4g	|- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )