Theorem dfsbcq2 3714

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 2069 and substitution for class variables df-sbc 3712. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3713. (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 3712	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 223	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 312	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2068   ∈ wcel 2108  {cab 2715  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712

This theorem is referenced by:  sbsbc  3715  sbc8g  3719  sbc2or  3720  sbceq1a  3722  sbc5ALT  3740  sbcng  3761  sbcimg  3762  sbcan  3763  sbcor  3764  sbcbig  3765  sbcim1  3767  sbcal  3776  sbcex2  3777  sbcel1v  3783  sbctt  3788  sbcralt  3801  sbcreu  3805  rspsbc  3808  rspesbca  3810  sbcel12  4339  sbceqg  4340  csbif  4513  rexreusng  4612  sbcbr123  5124  opelopabsb  5436  csbopab  5461  csbopabgALT  5462  iota4  6399  csbiota  6411  csbriota  7228  onminex  7629  findes  7723  nn0ind-raph  12350  uzind4s  12577  nn0min  31036  sbcrexgOLD  40523