Theorem dfsbcq2 3034

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 1811 and substitution for class variables df-sbc 3032. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3033. (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 2294	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2218	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3032	. . 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 1397   [wsb 1810   e. wcel 2202   {cab 2217   [.wsbc 3031

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-clab 2218  df-cleq 2224  df-clel 2227  df-sbc 3032

This theorem is referenced by:  sbsbc  3035  sbc8g  3039  sbceq1a  3041  sbc5  3055  sbcng  3072  sbcimg  3073  sbcan  3074  sbcang  3075  sbcor  3076  sbcorg  3077  sbcbig  3078  sbcal  3083  sbcalg  3084  sbcex2  3085  sbcexg  3086  sbcel1v  3094  sbctt  3098  sbcralt  3108  sbcrext  3109  sbcralg  3110  sbcreug  3112  rspsbc  3115  rspesbca  3117  sbcel12g  3142  sbceqg  3143  sbcbrg  4143  csbopabg  4167  opelopabsb  4354  findes  4701  iota4  5306  csbiotag  5319  csbriotag  5984  nn0ind-raph  9596  uzind4s  9823  bezoutlemmain  12568  bezoutlemex  12571