Theorem dfsbcq2 3270

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 1798 and substitution for class variables df-sbc 3268. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3269. (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 2517	. 2 |- ( y = A -> ( y e. { x | ph } <-> A e. { x | ph } ) )
2		df-clab 2438	. 2 |- ( y e. { x | ph } <-> [ y / x ] ph )
3		df-sbc 3268	. . 3 |- ( [. A / x ]. ph <-> A e. { x | ph } )
4	3	bicomi 206	. 2 |- ( A e. { x | ph } <-> [. A / x ]. ph )
5	1, 2, 4	3bitr3g 291	1 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   [wsb 1797   e. wcel 1887   {cab 2437   [.wsbc 3267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-clab 2438  df-cleq 2444  df-clel 2447  df-sbc 3268

This theorem is referenced by:  sbsbc  3271  sbc8g  3275  sbc2or  3276  sbceq1a  3278  sbc5  3292  sbcng  3308  sbcimg  3309  sbcan  3310  sbcor  3311  sbcbig  3312  sbcal  3317  sbcex2  3318  sbcel1v  3326  sbctt  3330  sbcralt  3340  sbcreu  3344  rspsbc  3346  rspesbca  3348  sbcel12  3772  sbceqg  3773  csbif  3931  sbcbr123  4454  opelopabsb  4711  csbopab  4733  csbopabgALT  4734  iota4  5564  csbiota  5575  csbriota  6264  onminex  6634  findes  6723  nn0ind-raph  11035  uzind4s  11219  nn0min  28384  sbcrexgOLD  35628  sbcangOLD  36890  sbcorgOLD  36891  sbcalgOLD  36903  sbcexgOLD  36904  sbcel12gOLD  36905  sbcel1gvOLD  37255