Theorem dfsbcq2 2907

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 1736 and substitution for class variables df-sbc 2905. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2906. (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 2200	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2124	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2905	. . 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 1331   e. wcel 1480   [wsb 1735   {cab 2123   [.wsbc 2904

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-clab 2124  df-cleq 2130  df-clel 2133  df-sbc 2905

This theorem is referenced by:  sbsbc  2908  sbc8g  2911  sbceq1a  2913  sbc5  2927  sbcng  2944  sbcimg  2945  sbcan  2946  sbcang  2947  sbcor  2948  sbcorg  2949  sbcbig  2950  sbcal  2955  sbcalg  2956  sbcex2  2957  sbcexg  2958  sbcel1v  2966  sbctt  2970  sbcralt  2980  sbcrext  2981  sbcralg  2982  sbcreug  2984  rspsbc  2986  rspesbca  2988  sbcel12g  3012  sbceqg  3013  sbcbrg  3977  csbopabg  4001  opelopabsb  4177  findes  4512  iota4  5101  csbiotag  5111  csbriotag  5735  nn0ind-raph  9161  uzind4s  9378  bezoutlemmain  11675  bezoutlemex  11678