Theorem dfsbcq 2964

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

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148  {cab 2163  [wsbc 2962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-sbc 2963

This theorem is referenced by:  sbceq1d  2967  sbc8g  2970  spsbc  2974  sbcco  2984  sbcco2  2985  sbcie2g  2996  elrabsf  3001  eqsbc1  3002  csbeq1  3060  sbcnestgf  3108  sbcco3g  3114  cbvralcsf  3119  cbvrexcsf  3120  findes  4602  ralrnmpt  5658  rexrnmpt  5659  findcard2  6888  findcard2s  6889  ac6sfi  6897  nn1suc  8937  uzind4s2  9590  indstr  9592  bezoutlemmain  11998  prmind2  12119