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 2100 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 2854	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2745	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3748	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 227	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 316	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099   ∈ wcel 2146  {cab 2744  [wsbc 3747

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clab 2745  df-cleq 2758  df-clel 2841  df-sbc 3748

This theorem is used 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  4379  sbceqg  4380  csbif  4550  rexreusng  4650  sbcbr123  5170  opelopabsb  5519  csbopab  5545  csbopabw  5546  iota4  6524  csbiota  6536  csbriota  7395  onminex  7810  findes  7906  nn0ind-raph  12714  uzind4s  12950  nn0min  33202