Theorem dfsbcq2 3005

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 1787 and substitution for class variables df-sbc 3003. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3004. (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 2269	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2193	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3003	. . 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 1373   [wsb 1786   e. wcel 2177   {cab 2192   [.wsbc 3002

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-clab 2193  df-cleq 2199  df-clel 2202  df-sbc 3003

This theorem is referenced by:  sbsbc  3006  sbc8g  3010  sbceq1a  3012  sbc5  3026  sbcng  3043  sbcimg  3044  sbcan  3045  sbcang  3046  sbcor  3047  sbcorg  3048  sbcbig  3049  sbcal  3054  sbcalg  3055  sbcex2  3056  sbcexg  3057  sbcel1v  3065  sbctt  3069  sbcralt  3079  sbcrext  3080  sbcralg  3081  sbcreug  3083  rspsbc  3085  rspesbca  3087  sbcel12g  3112  sbceqg  3113  sbcbrg  4106  csbopabg  4130  opelopabsb  4314  findes  4659  iota4  5260  csbiotag  5273  csbriotag  5925  nn0ind-raph  9510  uzind4s  9731  bezoutlemmain  12394  bezoutlemex  12397