Theorem dfsbcq2 3048

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 1812 and substitution for class variables df-sbc 3046. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3047. (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 2297	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2221	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3046	. . 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 1398   [wsb 1811   e. wcel 2205   {cab 2220   [.wsbc 3045

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-clab 2221  df-cleq 2227  df-clel 2230  df-sbc 3046

This theorem is referenced by:  sbsbc  3049  sbc8g  3053  sbceq1a  3055  sbc5  3069  sbcng  3086  sbcimg  3087  sbcan  3088  sbcang  3089  sbcor  3090  sbcorg  3091  sbcbig  3092  sbcal  3097  sbcalg  3098  sbcex2  3099  sbcexg  3100  sbcel1v  3108  sbctt  3112  sbcralt  3122  sbcrext  3123  sbcralg  3124  sbcreug  3126  rspsbc  3129  rspesbca  3131  sbcel12g  3156  sbceqg  3157  sbcbrg  4169  csbopabg  4193  opelopabsb  4383  findes  4730  iota4  5337  csbiotag  5350  csbriotag  6025  nn0ind-raph  9713  uzind4s  9940  bezoutlemmain  12719  bezoutlemex  12722