Theorem dfsbcq2 3186

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 1706 and substitution for class variables df-sbc 3184. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3185. (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 2501	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2428	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3184	. . 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 1364   [wsb 1705   e. wcel 1761   {cab 2427   [.wsbc 3183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-clab 2428  df-cleq 2434  df-clel 2437  df-sbc 3184

This theorem is referenced by:  sbsbc  3187  sbc8g  3191  sbc2or  3192  sbceq1a  3194  sbc5  3208  sbcng  3224  sbcimg  3225  sbcan  3226  sbcangOLD  3227  sbcor  3228  sbcorgOLD  3229  sbcbig  3230  sbcal  3235  sbcalgOLD  3236  sbcex2  3237  sbcexgOLD  3238  sbc3angOLD  3247  sbcel1v  3248  sbcel1gvOLD  3249  sbctt  3254  sbcralt  3264  sbcrexgOLD  3269  sbcreu  3270  sbcreugOLD  3271  rspsbc  3273  rspesbca  3275  sbcel12  3672  sbcel12gOLD  3673  sbceqg  3674  csbif  3836  csbifgOLD  3837  sbcbr123  4340  sbcbrgOLD  4341  opelopabsb  4597  csbopab  4618  csbopabgOLD  4619  iota4  5396  csbiota  5407  csbiotagOLD  5408  csbriota  6062  onminex  6417  findes  6505  nn0ind-raph  10738  uzind4s  10910  nn0min  26023