Theorem dfsbcq2 3768

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2064   ∈ wcel 2108  {cab 2713  [wsbc 3765

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766

This theorem is referenced by:  sbsbc  3769  sbc8g  3773  sbc2or  3774  sbceq1a  3776  sbc5ALT  3794  sbcng  3813  sbcimg  3814  sbcan  3815  sbcor  3816  sbcbig  3817  sbcim1  3819  sbcal  3825  sbcex2  3826  sbcel1v  3831  sbctt  3835  sbcralt  3847  sbcreu  3851  rspsbc  3854  rspesbca  3856  sbcel12  4386  sbceqg  4387  csbif  4558  rexreusng  4655  sbcbr123  5173  opelopabsb  5505  csbopab  5530  csbopabgALT  5531  iota4  6512  csbiota  6524  csbriota  7377  onminex  7796  findes  7896  nn0ind-raph  12693  uzind4s  12924  nn0min  32799  sbcrexgOLD  42808