Theorem dfsbcq2 2989

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 1774 and substitution for class variables df-sbc 2987. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2988. (Contributed by NM, 31-Dec-2016.)

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   [wsb 1773   e. wcel 2164   {cab 2179   [.wsbc 2986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-clab 2180  df-cleq 2186  df-clel 2189  df-sbc 2987

This theorem is referenced by:  sbsbc  2990  sbc8g  2994  sbceq1a  2996  sbc5  3010  sbcng  3027  sbcimg  3028  sbcan  3029  sbcang  3030  sbcor  3031  sbcorg  3032  sbcbig  3033  sbcal  3038  sbcalg  3039  sbcex2  3040  sbcexg  3041  sbcel1v  3049  sbctt  3053  sbcralt  3063  sbcrext  3064  sbcralg  3065  sbcreug  3067  rspsbc  3069  rspesbca  3071  sbcel12g  3096  sbceqg  3097  sbcbrg  4084  csbopabg  4108  opelopabsb  4291  findes  4636  iota4  5235  csbiotag  5248  csbriotag  5887  nn0ind-raph  9437  uzind4s  9658  bezoutlemmain  12138  bezoutlemex  12141