Theorem dfsbcq2 2818

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 1686 and substitution for class variables df-sbc 2816. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2817. (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 2141	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2068	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2816	. . 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 1284   e. wcel 1433   [wsb 1685   {cab 2067   [.wsbc 2815

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-clab 2068  df-cleq 2074  df-clel 2077  df-sbc 2816

This theorem is referenced by:  sbsbc  2819  sbc8g  2822  sbceq1a  2824  sbc5  2838  sbcng  2854  sbcimg  2855  sbcan  2856  sbcang  2857  sbcor  2858  sbcorg  2859  sbcbig  2860  sbcal  2865  sbcalg  2866  sbcex2  2867  sbcexg  2868  sbcel1v  2876  sbctt  2880  sbcralt  2890  sbcrext  2891  sbcralg  2892  sbcreug  2894  rspsbc  2896  rspesbca  2898  sbcel12g  2921  sbceqg  2922  sbcbrg  3834  csbopabg  3856  opelopabsb  4015  findes  4344  iota4  4905  csbiotag  4915  csbriotag  5500  nn0ind-raph  8464  uzind4s  8678  bezoutlemmain  10387  bezoutlemex  10390