Theorem dfsbcq2 3050

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 1649 and substitution for class variables df-sbc 3048. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3049. (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 2413	. 2 |- (y = A -> (y e. {x | ph} <-> A e. {x | ph}))
2		df-clab 2340	. 2 |- (y e. {x | ph} <-> [y / x]ph)
3		df-sbc 3048	. . 3 |- ( [.A / x ].ph <-> A e. {x | ph})
4	3	bicomi 193	. 2 |- (A e. {x | ph} <-> [.A / x ].ph)
5	1, 2, 4	3bitr3g 278	1 |- (y = A -> ([y / x]ph <-> [.A / x ].ph))

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642  [wsb 1648   e. wcel 1710  {cab 2339   [.wsbc 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-clab 2340  df-cleq 2346  df-clel 2349  df-sbc 3048

This theorem is referenced by:  sbsbc  3051  sbc8g  3054  sbc2or  3055  sbceq1a  3057  sbc5  3071  sbcng  3087  sbcimg  3088  sbcan  3089  sbcang  3090  sbcor  3091  sbcorg  3092  sbcbig  3093  sbcal  3094  sbcalg  3095  sbcex2  3096  sbcexg  3097  sbc3ang  3105  sbcel1gv  3106  sbcel2gv  3107  sbctt  3109  sbcralt  3119  sbcralg  3121  sbcrexg  3122  sbcreug  3123  rspsbc  3125  rspesbca  3127  sbcel12g  3152  sbceqg  3153  csbifg  3691  iota4  4358  csbiotag  4372  csbopabg  4638  sbcbrg  4686  opelopabsb  4698