Theorem dfsbcq2 2965

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 1763 and substitution for class variables df-sbc 2963. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2964. (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 2240	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2164	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 2963	. . 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 1353   [wsb 1762   e. wcel 2148   {cab 2163   [.wsbc 2962

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2963

This theorem is referenced by:  sbsbc  2966  sbc8g  2970  sbceq1a  2972  sbc5  2986  sbcng  3003  sbcimg  3004  sbcan  3005  sbcang  3006  sbcor  3007  sbcorg  3008  sbcbig  3009  sbcal  3014  sbcalg  3015  sbcex2  3016  sbcexg  3017  sbcel1v  3025  sbctt  3029  sbcralt  3039  sbcrext  3040  sbcralg  3041  sbcreug  3043  rspsbc  3045  rspesbca  3047  sbcel12g  3072  sbceqg  3073  sbcbrg  4055  csbopabg  4079  opelopabsb  4258  findes  4600  iota4  5193  csbiotag  5206  csbriotag  5838  nn0ind-raph  9364  uzind4s  9584  bezoutlemmain  11989  bezoutlemex  11992