Theorem dfsbcq 2817

Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42 and holds under both our definition and Quine's, provides us with a weak definition of the proper substitution of a class for a set. Since our df-sbc 2816 does not result in the same behavior as Quine's for proper classes, if we wished to avoid conflict with Quine's definition we could start with this theorem and dfsbcq2 2818 instead of df-sbc 2816. (dfsbcq2 2818 is needed because unlike Quine we do not overload the df-sb 1686 syntax.) As a consequence of these theorems, we can derive sbc8g 2822, which is a weaker version of df-sbc 2816 that leaves substitution undefined when 𝐴 is a proper class.

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2822, so we will allow direct use of df-sbc 2816. Proper substiution with a proper class is rarely needed, and when it is, we can simply use the expansion of Quine's definition. (Contributed by NM, 14-Apr-1995.)

Assertion

Ref	Expression
dfsbcq	⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))

Proof of Theorem dfsbcq

Step	Hyp	Ref	Expression
1		eleq1 2141	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}))
2		df-sbc 2816	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		df-sbc 2816	. 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})
4	1, 2, 3	3bitr4g 221	1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1284   ∈ wcel 1433  {cab 2067  [wsbc 2815

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077  df-sbc 2816

This theorem is referenced by:  sbceq1d  2820  sbc8g  2822  spsbc  2826  sbcco  2836  sbcco2  2837  sbcie2g  2847  elrabsf  2852  eqsbc3  2853  csbeq1  2911  sbcnestgf  2953  sbcco3g  2959  cbvralcsf  2964  cbvrexcsf  2965  findes  4344  ralrnmpt  5330  rexrnmpt  5331  findcard2  6373  findcard2s  6374  ac6sfi  6379  nn1suc  8058  uzind4s2  8679  indstr  8681  bezoutlemmain  10387  prmind2  10502