This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )