Theorem dfsbcq2 3189

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 1701 and substitution for class variables df-sbc 3187. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3188. (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 2503	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2430	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3187	. . 3 |- ( [. A / x ]. ph <-> A e. { x | ph } )
4	3	bicomi 202	. 2 |- ( A e. { x | ph } <-> [. A / x ]. ph )
5	1, 2, 4	3bitr3g 287	1 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   [wsb 1700   e. wcel 1756   {cab 2429   [.wsbc 3186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-clab 2430  df-cleq 2436  df-clel 2439  df-sbc 3187

This theorem is referenced by:  sbsbc  3190  sbc8g  3194  sbc2or  3195  sbceq1a  3197  sbc5  3211  sbcng  3227  sbcimg  3228  sbcan  3229  sbcangOLD  3230  sbcor  3231  sbcorgOLD  3232  sbcbig  3233  sbcal  3238  sbcalgOLD  3239  sbcex2  3240  sbcexgOLD  3241  sbc3angOLD  3250  sbcel1v  3251  sbcel1gvOLD  3252  sbctt  3257  sbcralt  3267  sbcrexgOLD  3272  sbcreu  3273  sbcreugOLD  3274  rspsbc  3276  rspesbca  3278  sbcel12  3675  sbcel12gOLD  3676  sbceqg  3677  csbif  3839  csbifgOLD  3840  sbcbr123  4343  sbcbrgOLD  4344  opelopabsb  4599  csbopab  4620  csbopabgALT  4621  iota4  5399  csbiota  5410  csbiotagOLD  5411  csbriota  6064  onminex  6418  findes  6506  nn0ind-raph  10742  uzind4s  10914  nn0min  26090