Theorem dfsbcq2 3746

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568  [wsb 2094   ∈ wcel 2141  {cab 2739  [wsbc 3743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3744

This theorem is referenced by:  sbsbc  3747  sbc8g  3751  sbc2or  3752  sbceq1a  3754  sbc5ALT  3772  sbcng  3790  sbcimg  3791  sbcan  3792  sbcor  3793  sbcbig  3794  sbcim1  3796  sbcal  3802  sbcex2  3803  sbcel1v  3808  sbctt  3812  sbcralt  3824  sbcreu  3828  rspsbc  3831  rspesbca  3833  sbcel12  4375  sbceqg  4376  csbif  4544  rexreusng  4644  sbcbr123  5164  opelopabsb  5514  csbopab  5540  csbopabw  5541  iota4  6517  csbiota  6529  csbriota  7382  onminex  7800  findes  7896  nn0ind-raph  12695  uzind4s  12931  nn0min  33131