Theorem dfsbcq2 2963

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2238	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2162	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 2961	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 132	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 222	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  [wsb 1760   ∈ wcel 2146  {cab 2161  [wsbc 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-clab 2162  df-cleq 2168  df-clel 2171  df-sbc 2961

This theorem is referenced by:  sbsbc  2964  sbc8g  2968  sbceq1a  2970  sbc5  2984  sbcng  3001  sbcimg  3002  sbcan  3003  sbcang  3004  sbcor  3005  sbcorg  3006  sbcbig  3007  sbcal  3012  sbcalg  3013  sbcex2  3014  sbcexg  3015  sbcel1v  3023  sbctt  3027  sbcralt  3037  sbcrext  3038  sbcralg  3039  sbcreug  3041  rspsbc  3043  rspesbca  3045  sbcel12g  3070  sbceqg  3071  sbcbrg  4052  csbopabg  4076  opelopabsb  4254  findes  4596  iota4  5188  csbiotag  5201  csbriotag  5833  nn0ind-raph  9341  uzind4s  9561  bezoutlemmain  11964  bezoutlemex  11967