Theorem dfsbcq2 3033

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  [wsb 1809   ∈ wcel 2201  {cab 2216  [wsbc 3030

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-clab 2217  df-cleq 2223  df-clel 2226  df-sbc 3031

This theorem is referenced by:  sbsbc  3034  sbc8g  3038  sbceq1a  3040  sbc5  3054  sbcng  3071  sbcimg  3072  sbcan  3073  sbcang  3074  sbcor  3075  sbcorg  3076  sbcbig  3077  sbcal  3082  sbcalg  3083  sbcex2  3084  sbcexg  3085  sbcel1v  3093  sbctt  3097  sbcralt  3107  sbcrext  3108  sbcralg  3109  sbcreug  3111  rspsbc  3114  rspesbca  3116  sbcel12g  3141  sbceqg  3142  sbcbrg  4144  csbopabg  4168  opelopabsb  4356  findes  4703  iota4  5308  csbiotag  5321  csbriotag  5990  nn0ind-raph  9602  uzind4s  9829  bezoutlemmain  12592  bezoutlemex  12595