Theorem dfsbcq2 3747

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2849	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2740	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3745	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 226	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 315	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  [wsb 2089   ∈ wcel 2141  {cab 2739  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3745

This theorem is referenced by:  sbsbc  3748  sbc8g  3752  sbc2or  3753  sbceq1a  3755  sbc5ALT  3773  sbcng  3791  sbcimg  3792  sbcan  3793  sbcor  3794  sbcbig  3795  sbcim1  3797  sbcal  3803  sbcex2  3804  sbcel1v  3809  sbctt  3813  sbcralt  3825  sbcreu  3829  rspsbc  3832  rspesbca  3834  sbcel12  4364  sbceqg  4365  csbif  4537  rexreusng  4637  sbcbr123  5153  opelopabsb  5499  csbopab  5524  csbopabw  5525  iota4  6496  csbiota  6508  csbriota  7362  onminex  7779  findes  7875  nn0ind-raph  12668  uzind4s  12904  nn0min  32971