Theorem dfsbcq2 3032

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 3030. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3031. (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 3030	. . 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 3029

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 3030

This theorem is referenced by:  sbsbc  3033  sbc8g  3037  sbceq1a  3039  sbc5  3053  sbcng  3070  sbcimg  3071  sbcan  3072  sbcang  3073  sbcor  3074  sbcorg  3075  sbcbig  3076  sbcal  3081  sbcalg  3082  sbcex2  3083  sbcexg  3084  sbcel1v  3092  sbctt  3096  sbcralt  3106  sbcrext  3107  sbcralg  3108  sbcreug  3110  rspsbc  3113  rspesbca  3115  sbcel12g  3140  sbceqg  3141  sbcbrg  4141  csbopabg  4165  opelopabsb  4352  findes  4699  iota4  5304  csbiotag  5317  csbriotag  5980  nn0ind-raph  9587  uzind4s  9814  bezoutlemmain  12559  bezoutlemex  12562