Theorem dfsbcq2 3732

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

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 3730

This theorem is referenced by:  sbsbc  3733  sbc8g  3737  sbc2or  3738  sbceq1a  3740  sbc5ALT  3758  sbcng  3777  sbcimg  3778  sbcan  3779  sbcor  3780  sbcbig  3781  sbcim1  3783  sbcal  3789  sbcex2  3790  sbcel1v  3795  sbctt  3799  sbcralt  3811  sbcreu  3815  rspsbc  3818  rspesbca  3820  sbcel12  4352  sbceqg  4353  csbif  4525  rexreusng  4624  sbcbr123  5140  opelopabsb  5476  csbopab  5501  csbopabgALT  5502  iota4  6471  csbiota  6483  csbriota  7330  onminex  7747  findes  7842  nn0ind-raph  12618  uzind4s  12847  nn0min  32914  sbcrexgOLD  43228