Theorem dfsbcq2 2761

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 1643 and substitution for class variables df-sbc 2759. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2760. (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 2097	. 2 ⊢ (y = A → (y ∈ {x ∣ φ} ↔ A ∈ {x ∣ φ}))
2		df-clab 2024	. 2 ⊢ (y ∈ {x ∣ φ} ↔ [y / x]φ)
3		df-sbc 2759	. . 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 1242   ∈ wcel 1390  [wsb 1642  {cab 2023  [wsbc 2758

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-clab 2024  df-cleq 2030  df-clel 2033  df-sbc 2759

This theorem is referenced by:  sbsbc  2762  sbc8g  2765  sbceq1a  2767  sbc5  2781  sbcng  2797  sbcimg  2798  sbcan  2799  sbcang  2800  sbcor  2801  sbcorg  2802  sbcbig  2803  sbcal  2804  sbcalg  2805  sbcex2  2806  sbcexg  2807  sbc3ang  2814  sbcel1gv  2815  sbctt  2818  sbcralt  2828  sbcrext  2829  sbcralg  2830  sbcrexg  2831  sbcreug  2832  rspsbc  2834  rspesbca  2836  sbcel12g  2859  sbceqg  2860  sbcbrg  3804  csbopabg  3826  opelopabsb  3988  findes  4269  iota4  4828  csbiotag  4838  csbriotag  5423  nn0ind-raph  8131  uzind4s  8309