Theorem dfsbcq2 3774

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2900	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2800	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3772	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 226	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 315	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533  [wsb 2065   ∈ wcel 2110  {cab 2799  [wsbc 3771

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772

This theorem is referenced by:  sbsbc  3775  sbc8g  3779  sbc2or  3780  sbceq1a  3782  sbc5  3799  sbcng  3818  sbcimg  3819  sbcan  3820  sbcor  3821  sbcbig  3822  sbcal  3832  sbcex2  3833  sbcel1v  3838  sbcel1vOLD  3839  sbctt  3843  sbcralt  3854  sbcreu  3858  rspsbc  3861  rspesbca  3863  sbcel12  4359  sbceqg  4360  csbif  4521  rexreusng  4610  sbcbr123  5112  opelopabsb  5409  csbopab  5434  csbopabgALT  5435  iota4  6330  csbiota  6342  csbriota  7123  onminex  7516  findes  7606  nn0ind-raph  12076  uzind4s  12302  nn0min  30531  sbcrexgOLD  39375