Theorem dfsbcq2 2949

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 1750 and substitution for class variables df-sbc 2947. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2948. (Contributed by NM, 31-Dec-2016.)

Assertion

Ref	Expression
dfsbcq2	⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2227	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2151	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 2947	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 131	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 221	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1342  [wsb 1749   ∈ wcel 2135  {cab 2150  [wsbc 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-clab 2151  df-cleq 2157  df-clel 2160  df-sbc 2947

This theorem is referenced by:  sbsbc  2950  sbc8g  2953  sbceq1a  2955  sbc5  2969  sbcng  2986  sbcimg  2987  sbcan  2988  sbcang  2989  sbcor  2990  sbcorg  2991  sbcbig  2992  sbcal  2997  sbcalg  2998  sbcex2  2999  sbcexg  3000  sbcel1v  3008  sbctt  3012  sbcralt  3022  sbcrext  3023  sbcralg  3024  sbcreug  3026  rspsbc  3028  rspesbca  3030  sbcel12g  3055  sbceqg  3056  sbcbrg  4030  csbopabg  4054  opelopabsb  4232  findes  4574  iota4  5165  csbiotag  5175  csbriotag  5804  nn0ind-raph  9299  uzind4s  9519  bezoutlemmain  11916  bezoutlemex  11919