Theorem sbccsb

Description: Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbccsb	|- ( [. A / x ]. ph <-> y e. [_ A / x ]_ { y | ph } )

Proof

Step	Hyp	Ref	Expression
1		abid	|- ( y e. { y | ph } <-> ph )
2	1	sbcbii	|- ( [. A / x ]. y e. { y | ph } <-> [. A / x ]. ph )
3		sbcel2	|- ( [. A / x ]. y e. { y | ph } <-> y e. [_ A / x ]_ { y | ph } )
4	2 3	bitr3i	|- ( [. A / x ]. ph <-> y e. [_ A / x ]_ { y | ph } )