Theorem dfsbcq2 2966

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  [wsb 1762   ∈ wcel 2148  {cab 2163  [wsbc 2963

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2964

This theorem is referenced by:  sbsbc  2967  sbc8g  2971  sbceq1a  2973  sbc5  2987  sbcng  3004  sbcimg  3005  sbcan  3006  sbcang  3007  sbcor  3008  sbcorg  3009  sbcbig  3010  sbcal  3015  sbcalg  3016  sbcex2  3017  sbcexg  3018  sbcel1v  3026  sbctt  3030  sbcralt  3040  sbcrext  3041  sbcralg  3042  sbcreug  3044  rspsbc  3046  rspesbca  3048  sbcel12g  3073  sbceqg  3074  sbcbrg  4058  csbopabg  4082  opelopabsb  4261  findes  4603  iota4  5197  csbiotag  5210  csbriotag  5843  nn0ind-raph  9370  uzind4s  9590  bezoutlemmain  11999  bezoutlemex  12002