Theorem dfsbcq 2939

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

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1335   ∈ wcel 2128  {cab 2143  [wsbc 2937

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153  df-sbc 2938

This theorem is referenced by:  sbceq1d  2942  sbc8g  2944  spsbc  2948  sbcco  2958  sbcco2  2959  sbcie2g  2970  elrabsf  2975  eqsbc3  2976  csbeq1  3034  sbcnestgf  3082  sbcco3g  3088  cbvralcsf  3093  cbvrexcsf  3094  findes  4564  ralrnmpt  5611  rexrnmpt  5612  findcard2  6836  findcard2s  6837  ac6sfi  6845  nn1suc  8857  uzind4s2  9507  indstr  9509  bezoutlemmain  11897  prmind2  12012