Theorem dfsbcq2 3747

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2065   ∈ wcel 2109  {cab 2707  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3745

This theorem is referenced by:  sbsbc  3748  sbc8g  3752  sbc2or  3753  sbceq1a  3755  sbc5ALT  3773  sbcng  3792  sbcimg  3793  sbcan  3794  sbcor  3795  sbcbig  3796  sbcim1  3798  sbcal  3804  sbcex2  3805  sbcel1v  3810  sbctt  3814  sbcralt  3826  sbcreu  3830  rspsbc  3833  rspesbca  3835  sbcel12  4364  sbceqg  4365  csbif  4536  rexreusng  4633  sbcbr123  5149  opelopabsb  5477  csbopab  5502  csbopabgALT  5503  iota4  6467  csbiota  6479  csbriota  7325  onminex  7742  findes  7840  nn0ind-raph  12594  uzind4s  12827  nn0min  32778  sbcrexgOLD  42758