Theorem dfsbcq2 2832

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 1690 and substitution for class variables df-sbc 2830. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2831. (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 2147	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2072	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2830	. . 3 |- ( [. A / x ]. ph <-> A e. { x | ph } )
4	3	bicomi 130	. 2 |- ( A e. { x | ph } <-> [. A / x ]. ph )
5	1, 2, 4	3bitr3g 220	1 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1287   e. wcel 1436   [wsb 1689   {cab 2071   [.wsbc 2829

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-clab 2072  df-cleq 2078  df-clel 2081  df-sbc 2830

This theorem is referenced by:  sbsbc  2833  sbc8g  2836  sbceq1a  2838  sbc5  2852  sbcng  2868  sbcimg  2869  sbcan  2870  sbcang  2871  sbcor  2872  sbcorg  2873  sbcbig  2874  sbcal  2879  sbcalg  2880  sbcex2  2881  sbcexg  2882  sbcel1v  2890  sbctt  2894  sbcralt  2904  sbcrext  2905  sbcralg  2906  sbcreug  2908  rspsbc  2910  rspesbca  2912  sbcel12g  2935  sbceqg  2936  sbcbrg  3869  csbopabg  3891  opelopabsb  4061  findes  4391  iota4  4964  csbiotag  4974  csbriotag  5581  nn0ind-raph  8796  uzind4s  9010  bezoutlemmain  10862  bezoutlemex  10865