Theorem dfsbcq2 3794

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  [wsb 2062   ∈ wcel 2106  {cab 2712  [wsbc 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792

This theorem is referenced by:  sbsbc  3795  sbc8g  3799  sbc2or  3800  sbceq1a  3802  sbc5ALT  3820  sbcng  3842  sbcimg  3843  sbcan  3844  sbcor  3845  sbcbig  3846  sbcim1  3848  sbcal  3855  sbcex2  3856  sbcel1v  3862  sbctt  3867  sbcralt  3881  sbcreu  3885  rspsbc  3888  rspesbca  3890  sbcel12  4417  sbceqg  4418  csbif  4588  rexreusng  4684  sbcbr123  5202  opelopabsb  5540  csbopab  5565  csbopabgALT  5566  iota4  6544  csbiota  6556  csbriota  7403  onminex  7822  findes  7923  nn0ind-raph  12716  uzind4s  12948  nn0min  32827  sbcrexgOLD  42773