Theorem dfsbcq2 3002

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  [wsb 1786   ∈ wcel 2177  {cab 2192  [wsbc 2999

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-clab 2193  df-cleq 2199  df-clel 2202  df-sbc 3000

This theorem is referenced by:  sbsbc  3003  sbc8g  3007  sbceq1a  3009  sbc5  3023  sbcng  3040  sbcimg  3041  sbcan  3042  sbcang  3043  sbcor  3044  sbcorg  3045  sbcbig  3046  sbcal  3051  sbcalg  3052  sbcex2  3053  sbcexg  3054  sbcel1v  3062  sbctt  3066  sbcralt  3076  sbcrext  3077  sbcralg  3078  sbcreug  3080  rspsbc  3082  rspesbca  3084  sbcel12g  3109  sbceqg  3110  sbcbrg  4102  csbopabg  4126  opelopabsb  4310  findes  4655  iota4  5256  csbiotag  5269  csbriotag  5919  nn0ind-raph  9497  uzind4s  9718  bezoutlemmain  12363  bezoutlemex  12366