Theorem dfsbcq2 3742

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2066   ∈ wcel 2110  {cab 2708  [wsbc 3739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3740

This theorem is referenced by:  sbsbc  3743  sbc8g  3747  sbc2or  3748  sbceq1a  3750  sbc5ALT  3768  sbcng  3787  sbcimg  3788  sbcan  3789  sbcor  3790  sbcbig  3791  sbcim1  3793  sbcal  3799  sbcex2  3800  sbcel1v  3805  sbctt  3809  sbcralt  3821  sbcreu  3825  rspsbc  3828  rspesbca  3830  sbcel12  4359  sbceqg  4360  csbif  4531  rexreusng  4630  sbcbr123  5143  opelopabsb  5468  csbopab  5493  csbopabgALT  5494  iota4  6458  csbiota  6470  csbriota  7313  onminex  7730  findes  7825  nn0ind-raph  12565  uzind4s  12798  nn0min  32793  sbcrexgOLD  42797