Theorem dfsbcq2

Description: This theorem, which is similar to Theorem 6.7 of Quine p. 42 and holds under both our definition and Quine's, relates logic substitution df-sb and substitution for class variables df-sbc . Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq . (Contributed by NM, 31-Dec-2016)

	Ref	Expression
Assertion	dfsbcq2	|- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab	|- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc	|- ( [. A / x ]. ph <-> A e. { x | ph } )
4	3	bicomi	|- ( A e. { x | ph } <-> [. A / x ]. ph )
5	1 2 4	3bitr3g	|- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )