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 2066 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 2819	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2708	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3777	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 223	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 312	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2065   ∈ wcel 2104  {cab 2707  [wsbc 3776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-clab 2708  df-cleq 2722  df-clel 2808  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  6523  csbiota  6535  csbriota  7383  onminex  7792  findes  7895  nn0ind-raph  12666  uzind4s  12896  nn0min  32293  sbcrexgOLD  41825