Theorem dfsbcq2 3049

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 3047. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3048. (Contributed by NM, 31-Dec-2016.)

Assertion

Ref	Expression
dfsbcq2	⊢ (y = A → ([y / x]φ ↔ [̣A / x]̣φ))

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2413	. 2 ⊢ (y = A → (y ∈ {x ∣ φ} ↔ A ∈ {x ∣ φ}))
2		df-clab 2340	. 2 ⊢ (y ∈ {x ∣ φ} ↔ [y / x]φ)
3		df-sbc 3047	. . 3 ⊢ ([̣A / x]̣φ ↔ A ∈ {x ∣ φ})
4	3	bicomi 193	. 2 ⊢ (A ∈ {x ∣ φ} ↔ [̣A / x]̣φ)
5	1, 2, 4	3bitr3g 278	1 ⊢ (y = A → ([y / x]φ ↔ [̣A / x]̣φ))

Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642  [wsb 1648   ∈ wcel 1710  {cab 2339  [̣wsbc 3046

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 3047

This theorem is referenced by:  sbsbc  3050  sbc8g  3053  sbc2or  3054  sbceq1a  3056  sbc5  3070  sbcng  3086  sbcimg  3087  sbcan  3088  sbcang  3089  sbcor  3090  sbcorg  3091  sbcbig  3092  sbcal  3093  sbcalg  3094  sbcex2  3095  sbcexg  3096  sbc3ang  3104  sbcel1gv  3105  sbcel2gv  3106  sbctt  3108  sbcralt  3118  sbcralg  3120  sbcrexg  3121  sbcreug  3122  rspsbc  3124  rspesbca  3126  sbcel12g  3151  sbceqg  3152  csbifg  3690  iota4  4357  csbiotag  4371  csbopabg  4637  sbcbrg  4685  opelopabsb  4697