Theorem dfsbcq 2911

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

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ∈ wcel 1480  {cab 2125  [wsbc 2909

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-sbc 2910

This theorem is referenced by:  sbceq1d  2914  sbc8g  2916  spsbc  2920  sbcco  2930  sbcco2  2931  sbcie2g  2942  elrabsf  2947  eqsbc3  2948  csbeq1  3006  sbcnestgf  3051  sbcco3g  3057  cbvralcsf  3062  cbvrexcsf  3063  findes  4517  ralrnmpt  5562  rexrnmpt  5563  findcard2  6783  findcard2s  6784  ac6sfi  6792  nn1suc  8739  uzind4s2  9386  indstr  9388  bezoutlemmain  11686  prmind2  11801