Theorem dfsbcq2 3779

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  [wsb 2068   ∈ wcel 2107  {cab 2710  [wsbc 3776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3777

This theorem is referenced by:  sbsbc  3780  sbc8g  3784  sbc2or  3785  sbceq1a  3787  sbc5ALT  3805  sbcng  3826  sbcimg  3827  sbcan  3828  sbcor  3829  sbcbig  3830  sbcim1  3832  sbcal  3840  sbcex2  3841  sbcel1v  3847  sbctt  3852  sbcralt  3865  sbcreu  3869  rspsbc  3872  rspesbca  3874  sbcel12  4407  sbceqg  4408  csbif  4584  rexreusng  4682  sbcbr123  5201  opelopabsb  5529  csbopab  5554  csbopabgALT  5555  iota4  6521  csbiota  6533  csbriota  7376  onminex  7785  findes  7888  nn0ind-raph  12658  uzind4s  12888  nn0min  32004  sbcrexgOLD  41456