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

Proof

Step	Hyp	Ref	Expression
1		csbab	|- [_ A / x ]_ { y | y = B } = { y | [. A / x ]. y = B }
2		sbceq2g	|- ( A e. V -> ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) )
3	2	abbidv	|- ( A e. V -> { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } )
4	1 3	syl5eq	|- ( A e. V -> [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } )
5		df-sn	|- { B } = { y | y = B }
6	5	csbeq2i	|- [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B }
7		df-sn	|- { [_ A / x ]_ B } = { y | y = [_ A / x ]_ B }
8	4 6 7	3eqtr4g	|- ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )