Theorem dfsbcq2 3334

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 1712 and substitution for class variables df-sbc 3332. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3333. (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 2539	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2453	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3332	. . 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 1379   [wsb 1711   e. wcel 1767   {cab 2452   [.wsbc 3331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-clab 2453  df-cleq 2459  df-clel 2462  df-sbc 3332

This theorem is referenced by:  sbsbc  3335  sbc8g  3339  sbc2or  3340  sbceq1a  3342  sbc5  3356  sbcng  3372  sbcimg  3373  sbcan  3374  sbcangOLD  3375  sbcor  3376  sbcorgOLD  3377  sbcbig  3378  sbcal  3383  sbcalgOLD  3384  sbcex2  3385  sbcexgOLD  3386  sbc3angOLD  3395  sbcel1v  3396  sbcel1gvOLD  3397  sbctt  3402  sbcralt  3412  sbcrexgOLD  3417  sbcreu  3418  sbcreugOLD  3419  rspsbc  3421  rspesbca  3423  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  csbif  3989  csbifgOLD  3990  sbcbr123  4498  sbcbrgOLD  4499  opelopabsb  4757  csbopab  4779  csbopabgALT  4780  iota4  5569  csbiota  5580  csbiotagOLD  5581  csbriota  6257  onminex  6626  findes  6714  nn0ind-raph  10961  uzind4s  11141  nn0min  27307