Theorem dfsbcq2 3054

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 1816 and substitution for class variables df-sbc 3052. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3053. (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 2301	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2225	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3052	. . 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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   [wsb 1815   e. wcel 2209   {cab 2224   [.wsbc 3051

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-clab 2225  df-cleq 2231  df-clel 2234  df-sbc 3052

This theorem is used by:  sbsbc  3055  sbc8g  3059  sbceq1a  3061  sbc5  3075  sbcng  3092  sbcimg  3093  sbcan  3094  sbcang  3095  sbcor  3096  sbcorg  3097  sbcbig  3098  sbcal  3103  sbcalg  3104  sbcex2  3105  sbcexg  3106  sbcel1v  3114  sbctt  3118  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcreug  3132  rspsbc  3135  rspesbca  3137  sbcel12g  3162  sbceqg  3163  sbcbrg  4185  csbopabg  4209  opelopabsb  4402  findes  4750  iota4  5357  csbiotag  5370  csbriotag  6052  nn0ind-raph  9763  uzind4s  9990  bezoutlemmain  12775  bezoutlemex  12778