Theorem dfsbcq2 3327

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 1745 and substitution for class variables df-sbc 3325. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3326. (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 2526	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2440	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3325	. . 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 1398   [wsb 1744   e. wcel 1823   {cab 2439   [.wsbc 3324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3325

This theorem is referenced by:  sbsbc  3328  sbc8g  3332  sbc2or  3333  sbceq1a  3335  sbc5  3349  sbcng  3365  sbcimg  3366  sbcan  3367  sbcor  3368  sbcbig  3369  sbcal  3374  sbcex2  3375  sbcel1v  3383  sbctt  3387  sbcralt  3397  sbcreu  3401  rspsbc  3403  rspesbca  3405  sbcel12  3822  sbceqg  3823  csbif  3979  sbcbr123  4490  opelopabsb  4746  csbopab  4768  csbopabgALT  4769  iota4  5552  csbiota  5563  csbriota  6244  onminex  6615  findes  6703  nn0ind-raph  10960  uzind4s  11142  nn0min  27845  sbcrexgOLD  30958  sbcangOLD  33690  sbcorgOLD  33691  sbcalgOLD  33703  sbcexgOLD  33704  sbcel12gOLD  33705  sbcel1gvOLD  34059