Theorem csbab

Description: Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005) (Revised by NM, 19-Aug-2018)

	Ref	Expression
Assertion	csbab	|- [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph }

Proof

Step	Hyp	Ref	Expression
1		df-clab	|- ( z e. { y | [. A / x ]. ph } <-> [ z / y ] [. A / x ]. ph )
2		sbsbc	|- ( [ z / y ] [. A / x ]. ph <-> [. z / y ]. [. A / x ]. ph )
3	1 2	bitri	|- ( z e. { y | [. A / x ]. ph } <-> [. z / y ]. [. A / x ]. ph )
4		sbccom	|- ( [. z / y ]. [. A / x ]. ph <-> [. A / x ]. [. z / y ]. ph )
5		df-clab	|- ( z e. { y | ph } <-> [ z / y ] ph )
6		sbsbc	|- ( [ z / y ] ph <-> [. z / y ]. ph )
7	5 6	bitri	|- ( z e. { y | ph } <-> [. z / y ]. ph )
8	7	sbcbii	|- ( [. A / x ]. z e. { y | ph } <-> [. A / x ]. [. z / y ]. ph )
9	4 8	bitr4i	|- ( [. z / y ]. [. A / x ]. ph <-> [. A / x ]. z e. { y | ph } )
10		sbcel2	|- ( [. A / x ]. z e. { y | ph } <-> z e. [_ A / x ]_ { y | ph } )
11	3 9 10	3bitrri	|- ( z e. [_ A / x ]_ { y | ph } <-> z e. { y | [. A / x ]. ph } )
12	11	eqriv	|- [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph }