Theorem dfsbcq2 3759

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2817	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2709	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3757	. . 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 2708  [wsbc 3756

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3757

This theorem is referenced by:  sbsbc  3760  sbc8g  3764  sbc2or  3765  sbceq1a  3767  sbc5ALT  3785  sbcng  3804  sbcimg  3805  sbcan  3806  sbcor  3807  sbcbig  3808  sbcim1  3810  sbcal  3816  sbcex2  3817  sbcel1v  3822  sbctt  3826  sbcralt  3838  sbcreu  3842  rspsbc  3845  rspesbca  3847  sbcel12  4377  sbceqg  4378  csbif  4549  rexreusng  4646  sbcbr123  5164  opelopabsb  5493  csbopab  5518  csbopabgALT  5519  iota4  6495  csbiota  6507  csbriota  7362  onminex  7781  findes  7879  nn0ind-raph  12641  uzind4s  12874  nn0min  32752  sbcrexgOLD  42780