Theorem dfsbcq 2915

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 2914 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 2916 instead of df-sbc 2914. (dfsbcq2 2916 is needed because unlike Quine we do not overload the df-sb 1737 syntax.) As a consequence of these theorems, we can derive sbc8g 2920, which is a weaker version of df-sbc 2914 that leaves substitution undefined when 𝐴 is a proper class.

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2920, so we will allow direct use of df-sbc 2914. 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 2203	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}))
2		df-sbc 2914	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		df-sbc 2914	. 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})
4	1, 2, 3	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   ∈ wcel 1481  {cab 2126  [wsbc 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136  df-sbc 2914

This theorem is referenced by:  sbceq1d  2918  sbc8g  2920  spsbc  2924  sbcco  2934  sbcco2  2935  sbcie2g  2946  elrabsf  2951  eqsbc3  2952  csbeq1  3010  sbcnestgf  3056  sbcco3g  3062  cbvralcsf  3067  cbvrexcsf  3068  findes  4525  ralrnmpt  5570  rexrnmpt  5571  findcard2  6791  findcard2s  6792  ac6sfi  6800  nn1suc  8763  uzind4s2  9413  indstr  9415  bezoutlemmain  11722  prmind2  11837