Theorem dfsbcq2 2865

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 1704 and substitution for class variables df-sbc 2863. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2864. (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 2162	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2087	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2863	. . 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 1299   e. wcel 1448   [wsb 1703   {cab 2086   [.wsbc 2862

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-clab 2087  df-cleq 2093  df-clel 2096  df-sbc 2863

This theorem is referenced by:  sbsbc  2866  sbc8g  2869  sbceq1a  2871  sbc5  2885  sbcng  2901  sbcimg  2902  sbcan  2903  sbcang  2904  sbcor  2905  sbcorg  2906  sbcbig  2907  sbcal  2912  sbcalg  2913  sbcex2  2914  sbcexg  2915  sbcel1v  2923  sbctt  2927  sbcralt  2937  sbcrext  2938  sbcralg  2939  sbcreug  2941  rspsbc  2943  rspesbca  2945  sbcel12g  2968  sbceqg  2969  sbcbrg  3924  csbopabg  3946  opelopabsb  4120  findes  4455  iota4  5042  csbiotag  5052  csbriotag  5674  nn0ind-raph  9020  uzind4s  9235  bezoutlemmain  11479  bezoutlemex  11482