Theorem dfsbcq2 2767

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 1646 and substitution for class variables df-sbc 2765. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2766. (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 2100	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2027	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2765	. . 3 |- ( [. A / x ]. ph <-> A e. { x | ph } )
4	3	bicomi 123	. 2 |- ( A e. { x | ph } <-> [. A / x ]. ph )
5	1, 2, 4	3bitr3g 211	1 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 98   = wceq 1243   e. wcel 1393   [wsb 1645   {cab 2026   [.wsbc 2764

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-clab 2027  df-cleq 2033  df-clel 2036  df-sbc 2765

This theorem is referenced by:  sbsbc  2768  sbc8g  2771  sbceq1a  2773  sbc5  2787  sbcng  2803  sbcimg  2804  sbcan  2805  sbcang  2806  sbcor  2807  sbcorg  2808  sbcbig  2809  sbcal  2810  sbcalg  2811  sbcex2  2812  sbcexg  2813  sbc3ang  2820  sbcel1gv  2821  sbctt  2824  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcreug  2838  rspsbc  2840  rspesbca  2842  sbcel12g  2865  sbceqg  2866  sbcbrg  3813  csbopabg  3835  opelopabsb  3997  findes  4326  iota4  4885  csbiotag  4895  csbriotag  5480  nn0ind-raph  8355  uzind4s  8533