Theorem dfsbcq2 3031

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 1809 and substitution for class variables df-sbc 3029. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3030. (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 2292	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2216	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3029	. . 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 1395   [wsb 1808   e. wcel 2200   {cab 2215   [.wsbc 3028

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-clab 2216  df-cleq 2222  df-clel 2225  df-sbc 3029

This theorem is referenced by:  sbsbc  3032  sbc8g  3036  sbceq1a  3038  sbc5  3052  sbcng  3069  sbcimg  3070  sbcan  3071  sbcang  3072  sbcor  3073  sbcorg  3074  sbcbig  3075  sbcal  3080  sbcalg  3081  sbcex2  3082  sbcexg  3083  sbcel1v  3091  sbctt  3095  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcreug  3109  rspsbc  3112  rspesbca  3114  sbcel12g  3139  sbceqg  3140  sbcbrg  4137  csbopabg  4161  opelopabsb  4347  findes  4694  iota4  5297  csbiotag  5310  csbriotag  5967  nn0ind-raph  9560  uzind4s  9781  bezoutlemmain  12514  bezoutlemex  12517