Theorem dfsbcq2 3750

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2853	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2744	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3748	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 227	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 316	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563  [wsb 2093   ∈ wcel 2145  {cab 2743  [wsbc 3747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748

This theorem is referenced by:  sbsbc  3751  sbc8g  3755  sbc2or  3756  sbceq1a  3758  sbc5ALT  3776  sbcng  3794  sbcimg  3795  sbcan  3796  sbcor  3797  sbcbig  3798  sbcim1  3800  sbcal  3806  sbcex2  3807  sbcel1v  3812  sbctt  3816  sbcralt  3828  sbcreu  3832  rspsbc  3835  rspesbca  3837  sbcel12  4368  sbceqg  4369  csbif  4541  rexreusng  4641  sbcbr123  5159  opelopabsb  5505  csbopab  5531  csbopabw  5532  iota4  6506  csbiota  6518  csbriota  7372  onminex  7789  findes  7885  nn0ind-raph  12687  uzind4s  12923  nn0min  33078