Theorem dfsbcq2 2958

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 1756 and substitution for class variables df-sbc 2956. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2957. (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 2233	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2157	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2956	. . 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 1348   [wsb 1755   e. wcel 2141   {cab 2156   [.wsbc 2955

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-clab 2157  df-cleq 2163  df-clel 2166  df-sbc 2956

This theorem is referenced by:  sbsbc  2959  sbc8g  2962  sbceq1a  2964  sbc5  2978  sbcng  2995  sbcimg  2996  sbcan  2997  sbcang  2998  sbcor  2999  sbcorg  3000  sbcbig  3001  sbcal  3006  sbcalg  3007  sbcex2  3008  sbcexg  3009  sbcel1v  3017  sbctt  3021  sbcralt  3031  sbcrext  3032  sbcralg  3033  sbcreug  3035  rspsbc  3037  rspesbca  3039  sbcel12g  3064  sbceqg  3065  sbcbrg  4043  csbopabg  4067  opelopabsb  4245  findes  4587  iota4  5178  csbiotag  5191  csbriotag  5821  nn0ind-raph  9329  uzind4s  9549  bezoutlemmain  11953  bezoutlemex  11956