Theorem dfsbcq2 3741

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 3739. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3740. (Contributed by NM, 31-Dec-2016.)

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2067   ∈ wcel 2113  {cab 2711  [wsbc 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clab 2712  df-cleq 2725  df-clel 2808  df-sbc 3739

This theorem is referenced by:  sbsbc  3742  sbc8g  3746  sbc2or  3747  sbceq1a  3749  sbc5ALT  3767  sbcng  3786  sbcimg  3787  sbcan  3788  sbcor  3789  sbcbig  3790  sbcim1  3792  sbcal  3798  sbcex2  3799  sbcel1v  3804  sbctt  3808  sbcralt  3820  sbcreu  3824  rspsbc  3827  rspesbca  3829  sbcel12  4362  sbceqg  4363  csbif  4534  rexreusng  4633  sbcbr123  5149  opelopabsb  5475  csbopab  5500  csbopabgALT  5501  iota4  6470  csbiota  6482  csbriota  7327  onminex  7744  findes  7839  nn0ind-raph  12583  uzind4s  12816  nn0min  32814  sbcrexgOLD  42892