Theorem dfsbcq2 3258

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 1806 and substitution for class variables df-sbc 3256. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3257. (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 2537	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2458	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3256	. . 3 |- ( [. A / x ]. ph <-> A e. { x | ph } )
4	3	bicomi 207	. 2 |- ( A e. { x | ph } <-> [. A / x ]. ph )
5	1, 2, 4	3bitr3g 295	1 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1452   [wsb 1805   e. wcel 1904   {cab 2457   [.wsbc 3255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-clab 2458  df-cleq 2464  df-clel 2467  df-sbc 3256

This theorem is referenced by:  sbsbc  3259  sbc8g  3263  sbc2or  3264  sbceq1a  3266  sbc5  3280  sbcng  3296  sbcimg  3297  sbcan  3298  sbcor  3299  sbcbig  3300  sbcal  3305  sbcex2  3306  sbcel1v  3314  sbctt  3318  sbcralt  3328  sbcreu  3332  rspsbc  3334  rspesbca  3336  sbcel12  3776  sbceqg  3777  csbif  3922  sbcbr123  4447  opelopabsb  4711  csbopab  4733  csbopabgALT  4734  iota4  5571  csbiota  5582  csbriota  6282  onminex  6653  findes  6742  nn0ind-raph  11058  uzind4s  11242  nn0min  28459  sbcrexgOLD  35699  sbcangOLD  36960  sbcorgOLD  36961  sbcalgOLD  36973  sbcexgOLD  36974  sbcel12gOLD  36975  sbcel1gvOLD  37318