Theorem dfsbcq2 3047

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  [wsb 1811   ∈ wcel 2205  {cab 2220  [wsbc 3044

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-clab 2221  df-cleq 2227  df-clel 2230  df-sbc 3045

This theorem is referenced by:  sbsbc  3048  sbc8g  3052  sbceq1a  3054  sbc5  3068  sbcng  3085  sbcimg  3086  sbcan  3087  sbcang  3088  sbcor  3089  sbcorg  3090  sbcbig  3091  sbcal  3096  sbcalg  3097  sbcex2  3098  sbcexg  3099  sbcel1v  3107  sbctt  3111  sbcralt  3121  sbcrext  3122  sbcralg  3123  sbcreug  3125  rspsbc  3128  rspesbca  3130  sbcel12g  3155  sbceqg  3156  sbcbrg  4166  csbopabg  4190  opelopabsb  4380  findes  4727  iota4  5334  csbiotag  5347  csbriotag  6019  nn0ind-raph  9701  uzind4s  9928  bezoutlemmain  12702  bezoutlemex  12705