Theorem csbid

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

	Ref	Expression
Assertion	csbid	|- [_ x / x ]_ A = A

Proof

Step	Hyp	Ref	Expression
1		df-csb	|- [_ x / x ]_ A = { y | [. x / x ]. y e. A }
2		sbcid	|- ( [. x / x ]. y e. A <-> y e. A )
3	2	abbii	|- { y | [. x / x ]. y e. A } = { y | y e. A }
4		abid2	|- { y | y e. A } = A
5	1 3 4	3eqtri	|- [_ x / x ]_ A = A