Theorem dfsbcq2 3744

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 3742. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3743. (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 3742	. . 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 3741

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 3742

This theorem is referenced by:  sbsbc  3745  sbc8g  3749  sbc2or  3750  sbceq1a  3752  sbc5ALT  3770  sbcng  3789  sbcimg  3790  sbcan  3791  sbcor  3792  sbcbig  3793  sbcim1  3795  sbcal  3801  sbcex2  3802  sbcel1v  3807  sbctt  3811  sbcralt  3823  sbcreu  3827  rspsbc  3830  rspesbca  3832  sbcel12  4364  sbceqg  4365  csbif  4538  rexreusng  4637  sbcbr123  5153  opelopabsb  5479  csbopab  5504  csbopabgALT  5505  iota4  6474  csbiota  6486  csbriota  7332  onminex  7749  findes  7844  nn0ind-raph  12596  uzind4s  12825  nn0min  32882  sbcrexgOLD  43063