Theorem dfsbcq2 2967

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 2965. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2966. (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 2965	. . 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 2964

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 2965

This theorem is referenced by:  sbsbc  2968  sbc8g  2972  sbceq1a  2974  sbc5  2988  sbcng  3005  sbcimg  3006  sbcan  3007  sbcang  3008  sbcor  3009  sbcorg  3010  sbcbig  3011  sbcal  3016  sbcalg  3017  sbcex2  3018  sbcexg  3019  sbcel1v  3027  sbctt  3031  sbcralt  3041  sbcrext  3042  sbcralg  3043  sbcreug  3045  rspsbc  3047  rspesbca  3049  sbcel12g  3074  sbceqg  3075  sbcbrg  4059  csbopabg  4083  opelopabsb  4262  findes  4604  iota4  5198  csbiotag  5211  csbriotag  5845  nn0ind-raph  9372  uzind4s  9592  bezoutlemmain  12001  bezoutlemex  12004