Theorem dfsbcq2 3436

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2688	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2608	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3434	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 214	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 302	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1482  [wsb 1879   ∈ wcel 1989  {cab 2607  [wsbc 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-clab 2608  df-cleq 2614  df-clel 2617  df-sbc 3434

This theorem is referenced by:  sbsbc  3437  sbc8g  3441  sbc2or  3442  sbceq1a  3444  sbc5  3458  sbcng  3474  sbcimg  3475  sbcan  3476  sbcor  3477  sbcbig  3478  sbcal  3483  sbcex2  3484  sbcel1v  3493  sbctt  3498  sbcralt  3508  sbcreu  3513  rspsbc  3516  rspesbca  3518  sbcel12  3981  sbceqg  3982  csbif  4136  sbcbr123  4704  opelopabsb  4983  csbopab  5006  csbopabgALT  5007  iota4  5867  csbiota  5879  csbriota  6620  onminex  7004  findes  7093  nn0ind-raph  11474  uzind4s  11745  nn0min  29552  sbcrexgOLD  37175  sbcangOLD  38565  sbcorgOLD  38566  sbcalgOLD  38578  sbcexgOLD  38579  sbcel12gOLD  38580  sbcel1gvOLD  38920