Theorem dfsbcq2 3719

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2826	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2716	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3717	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 223	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 313	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2067   ∈ wcel 2106  {cab 2715  [wsbc 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clab 2716  df-cleq 2730  df-clel 2816  df-sbc 3717

This theorem is referenced by:  sbsbc  3720  sbc8g  3724  sbc2or  3725  sbceq1a  3727  sbc5ALT  3745  sbcng  3766  sbcimg  3767  sbcan  3768  sbcor  3769  sbcbig  3770  sbcim1  3772  sbcal  3780  sbcex2  3781  sbcel1v  3787  sbctt  3792  sbcralt  3805  sbcreu  3809  rspsbc  3812  rspesbca  3814  sbcel12  4342  sbceqg  4343  csbif  4516  rexreusng  4615  sbcbr123  5128  opelopabsb  5443  csbopab  5468  csbopabgALT  5469  iota4  6414  csbiota  6426  csbriota  7248  onminex  7652  findes  7749  nn0ind-raph  12420  uzind4s  12648  nn0min  31134  sbcrexgOLD  40607