Theorem dfsbcq2 3807

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  [wsb 2064   ∈ wcel 2108  {cab 2717  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805

This theorem is referenced by:  sbsbc  3808  sbc8g  3812  sbc2or  3813  sbceq1a  3815  sbc5ALT  3833  sbcng  3855  sbcimg  3856  sbcan  3857  sbcor  3858  sbcbig  3859  sbcim1  3861  sbcal  3868  sbcex2  3869  sbcel1v  3875  sbctt  3880  sbcralt  3894  sbcreu  3898  rspsbc  3901  rspesbca  3903  sbcel12  4434  sbceqg  4435  csbif  4605  rexreusng  4703  sbcbr123  5220  opelopabsb  5549  csbopab  5574  csbopabgALT  5575  iota4  6554  csbiota  6566  csbriota  7420  onminex  7838  findes  7940  nn0ind-raph  12743  uzind4s  12973  nn0min  32824  sbcrexgOLD  42741