Theorem dfsbcq2 3756

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 3754. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3755. (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 3754	. . 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 3753

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 3754

This theorem is referenced by:  sbsbc  3757  sbc8g  3761  sbc2or  3762  sbceq1a  3764  sbc5ALT  3782  sbcng  3801  sbcimg  3802  sbcan  3803  sbcor  3804  sbcbig  3805  sbcim1  3807  sbcal  3813  sbcex2  3814  sbcel1v  3819  sbctt  3823  sbcralt  3835  sbcreu  3839  rspsbc  3842  rspesbca  3844  sbcel12  4374  sbceqg  4375  csbif  4546  rexreusng  4643  sbcbr123  5161  opelopabsb  5490  csbopab  5515  csbopabgALT  5516  iota4  6492  csbiota  6504  csbriota  7359  onminex  7778  findes  7876  nn0ind-raph  12634  uzind4s  12867  nn0min  32745  sbcrexgOLD  42773