Theorem dfsbcq2 3791

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2829	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2715	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3789	. . 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 2714  [wsbc 3788

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789

This theorem is referenced by:  sbsbc  3792  sbc8g  3796  sbc2or  3797  sbceq1a  3799  sbc5ALT  3817  sbcng  3836  sbcimg  3837  sbcan  3838  sbcor  3839  sbcbig  3840  sbcim1  3842  sbcal  3849  sbcex2  3850  sbcel1v  3856  sbctt  3860  sbcralt  3872  sbcreu  3876  rspsbc  3879  rspesbca  3881  sbcel12  4411  sbceqg  4412  csbif  4583  rexreusng  4679  sbcbr123  5197  opelopabsb  5535  csbopab  5560  csbopabgALT  5561  iota4  6542  csbiota  6554  csbriota  7403  onminex  7822  findes  7922  nn0ind-raph  12718  uzind4s  12950  nn0min  32822  sbcrexgOLD  42796