Theorem dfsbcq2 3780

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

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 3778

This theorem is referenced by:  sbsbc  3781  sbc8g  3785  sbc2or  3786  sbceq1a  3788  sbc5ALT  3806  sbcng  3827  sbcimg  3828  sbcan  3829  sbcor  3830  sbcbig  3831  sbcim1  3833  sbcal  3841  sbcex2  3842  sbcel1v  3848  sbctt  3853  sbcralt  3866  sbcreu  3870  rspsbc  3873  rspesbca  3875  sbcel12  4408  sbceqg  4409  csbif  4585  rexreusng  4683  sbcbr123  5202  opelopabsb  5530  csbopab  5555  csbopabgALT  5556  iota4  6522  csbiota  6534  csbriota  7378  onminex  7787  findes  7890  nn0ind-raph  12659  uzind4s  12889  nn0min  32014  sbcrexgOLD  41509