Theorem dfsbcq2 3438

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2689	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2609	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3436	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 214	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 302	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  [wsb 1880   ∈ wcel 1990  {cab 2608  [wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436

This theorem is referenced by:  sbsbc  3439  sbc8g  3443  sbc2or  3444  sbceq1a  3446  sbc5  3460  sbcng  3476  sbcimg  3477  sbcan  3478  sbcor  3479  sbcbig  3480  sbcal  3485  sbcex2  3486  sbcel1v  3495  sbctt  3500  sbcralt  3510  sbcreu  3515  rspsbc  3518  rspesbca  3520  sbcel12  3983  sbceqg  3984  csbif  4138  sbcbr123  4706  opelopabsb  4985  csbopab  5008  csbopabgALT  5009  iota4  5869  csbiota  5881  csbriota  6623  onminex  7007  findes  7096  nn0ind-raph  11477  uzind4s  11748  nn0min  29567  sbcrexgOLD  37349  sbcangOLD  38739  sbcorgOLD  38740  sbcalgOLD  38752  sbcexgOLD  38753  sbcel12gOLD  38754  sbcel1gvOLD  39094