Theorem csb2

Description: Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that x can be free in B but cannot occur in A . (Contributed by NM, 2-Dec-2013)

	Ref	Expression
Assertion	csb2	|- [_ A / x ]_ B = { y | E. x ( x = A /\ y e. B ) }

Proof

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