Theorem dfsbcq2 2988

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364  [wsb 1773   ∈ wcel 2164  {cab 2179  [wsbc 2985

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-clab 2180  df-cleq 2186  df-clel 2189  df-sbc 2986

This theorem is referenced by:  sbsbc  2989  sbc8g  2993  sbceq1a  2995  sbc5  3009  sbcng  3026  sbcimg  3027  sbcan  3028  sbcang  3029  sbcor  3030  sbcorg  3031  sbcbig  3032  sbcal  3037  sbcalg  3038  sbcex2  3039  sbcexg  3040  sbcel1v  3048  sbctt  3052  sbcralt  3062  sbcrext  3063  sbcralg  3064  sbcreug  3066  rspsbc  3068  rspesbca  3070  sbcel12g  3095  sbceqg  3096  sbcbrg  4083  csbopabg  4107  opelopabsb  4290  findes  4635  iota4  5234  csbiotag  5247  csbriotag  5886  nn0ind-raph  9434  uzind4s  9655  bezoutlemmain  12135  bezoutlemex  12138