Theorem dfsbcq2 3588

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1630  [wsb 2048   ∈ wcel 2144  {cab 2756  [wsbc 3585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1852  df-clab 2757  df-cleq 2763  df-clel 2766  df-sbc 3586

This theorem is referenced by:  sbsbc  3589  sbc8g  3593  sbc2or  3594  sbceq1a  3596  sbc5  3610  sbcng  3626  sbcimg  3627  sbcan  3628  sbcor  3629  sbcbig  3630  sbcal  3635  sbcex2  3636  sbcel1v  3644  sbctt  3648  sbcralt  3658  sbcreu  3662  rspsbc  3665  rspesbca  3667  sbcel12  4125  sbceqg  4126  csbif  4275  sbcbr123  4838  opelopabsb  5118  csbopab  5141  csbopabgALT  5142  iota4  6012  csbiota  6024  csbriota  6765  onminex  7153  findes  7242  nn0ind-raph  11678  uzind4s  11949  nn0min  29901  sbcrexgOLD  37868  sbcangOLD  39258  sbcorgOLD  39259  sbcalgOLD  39271  sbcexgOLD  39272  sbcel12gOLD  39273  sbcel1gvOLD  39610