Theorem dfsbcq2 3745

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068   ∈ wcel 2114  {cab 2715  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3743

This theorem is referenced by:  sbsbc  3746  sbc8g  3750  sbc2or  3751  sbceq1a  3753  sbc5ALT  3771  sbcng  3790  sbcimg  3791  sbcan  3792  sbcor  3793  sbcbig  3794  sbcim1  3796  sbcal  3802  sbcex2  3803  sbcel1v  3808  sbctt  3812  sbcralt  3824  sbcreu  3828  rspsbc  3831  rspesbca  3833  sbcel12  4365  sbceqg  4366  csbif  4539  rexreusng  4638  sbcbr123  5154  opelopabsb  5486  csbopab  5511  csbopabgALT  5512  iota4  6481  csbiota  6493  csbriota  7340  onminex  7757  findes  7852  nn0ind-raph  12604  uzind4s  12833  nn0min  32911  sbcrexgOLD  43131