Theorem dfsbcq2 3741

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2848	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2739	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3739	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 227	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 316	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  [wsb 2098   ∈ wcel 2144  {cab 2738  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739

This theorem is used by:  sbsbc  3742  sbc8g  3746  sbc2or  3747  sbceq1a  3749  sbc5ALT  3767  sbcng  3785  sbcimg  3786  sbcan  3787  sbcor  3788  sbcbig  3789  sbcim1  3791  sbcal  3797  sbcex2  3798  sbcel1v  3803  sbctt  3807  sbcralt  3818  sbcreu  3822  rspsbc  3825  rspesbca  3827  sbcel12  4368  sbceqg  4369  csbif  4539  rexreusng  4636  sbcbr123  5159  opelopabsb  5503  csbopab  5529  csbopabw  5530  iota4  6519  csbiota  6532  csbriota  7393  onminex  7817  findes  7913  nn0ind-raph  12803  uzind4s  13039  nn0min  33459