Theorem dfsbcq2 2980

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 1774 and substitution for class variables df-sbc 2978. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2979. (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 2252	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2176	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2978	. . 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 1364   [wsb 1773   e. wcel 2160   {cab 2175   [.wsbc 2977

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-clab 2176  df-cleq 2182  df-clel 2185  df-sbc 2978

This theorem is referenced by:  sbsbc  2981  sbc8g  2985  sbceq1a  2987  sbc5  3001  sbcng  3018  sbcimg  3019  sbcan  3020  sbcang  3021  sbcor  3022  sbcorg  3023  sbcbig  3024  sbcal  3029  sbcalg  3030  sbcex2  3031  sbcexg  3032  sbcel1v  3040  sbctt  3044  sbcralt  3054  sbcrext  3055  sbcralg  3056  sbcreug  3058  rspsbc  3060  rspesbca  3062  sbcel12g  3087  sbceqg  3088  sbcbrg  4075  csbopabg  4099  opelopabsb  4281  findes  4623  iota4  5218  csbiotag  5231  csbriotag  5868  nn0ind-raph  9405  uzind4s  9626  bezoutlemmain  12040  bezoutlemex  12043