Theorem dfsbcq2 2744

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 1628 and substitution for class variables df-sbc 2742. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2743. (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 2082	. 2 ⊢ (y = A → (y ∈ {x ∣ φ} ↔ A ∈ {x ∣ φ}))
2		df-clab 2009	. 2 ⊢ (y ∈ {x ∣ φ} ↔ [y / x]φ)
3		df-sbc 2742	. . 3 ⊢ ([A / x]φ ↔ A ∈ {x ∣ φ})
4	3	bicomi 123	. 2 ⊢ (A ∈ {x ∣ φ} ↔ [A / x]φ)
5	1, 2, 4	3bitr3g 211	1 ⊢ (y = A → ([y / x]φ ↔ [A / x]φ))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1228   ∈ wcel 1374  [wsb 1627  {cab 2008  [wsbc 2741

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-clab 2009  df-cleq 2015  df-clel 2018  df-sbc 2742

This theorem is referenced by:  sbsbc  2745  sbc8g  2748  sbceq1a  2750  sbc5  2764  sbcng  2780  sbcimg  2781  sbcan  2782  sbcang  2783  sbcor  2784  sbcorg  2785  sbcbig  2786  sbcal  2787  sbcalg  2788  sbcex2  2789  sbcexg  2790  sbc3ang  2797  sbcel1gv  2798  sbctt  2801  sbcralt  2811  sbcrext  2812  sbcralg  2813  sbcrexg  2814  sbcreug  2815  rspsbc  2817  rspesbca  2819  sbcel12g  2842  sbceqg  2843  sbcbrg  3787  csbopabg  3809  opelopabsb  3971  findes  4253  iota4  4812  csbiotag  4822  csbriotag  5404