Theorem dfsbcq2 2954

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 1751 and substitution for class variables df-sbc 2952. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2953. (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 2229	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2152	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2952	. . 3 |- ( [. A / x ]. ph <-> A e. { x | ph } )
4	3	bicomi 131	. 2 |- ( A e. { x | ph } <-> [. A / x ]. ph )
5	1, 2, 4	3bitr3g 221	1 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343   [wsb 1750   e. wcel 2136   {cab 2151   [.wsbc 2951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-clab 2152  df-cleq 2158  df-clel 2161  df-sbc 2952

This theorem is referenced by:  sbsbc  2955  sbc8g  2958  sbceq1a  2960  sbc5  2974  sbcng  2991  sbcimg  2992  sbcan  2993  sbcang  2994  sbcor  2995  sbcorg  2996  sbcbig  2997  sbcal  3002  sbcalg  3003  sbcex2  3004  sbcexg  3005  sbcel1v  3013  sbctt  3017  sbcralt  3027  sbcrext  3028  sbcralg  3029  sbcreug  3031  rspsbc  3033  rspesbca  3035  sbcel12g  3060  sbceqg  3061  sbcbrg  4036  csbopabg  4060  opelopabsb  4238  findes  4580  iota4  5171  csbiotag  5181  csbriotag  5810  nn0ind-raph  9308  uzind4s  9528  bezoutlemmain  11931  bezoutlemex  11934