ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfsbcq GIF version

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2887, so we will allow direct use of df-sbc 2881. 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
StepHypRef Expression
1 eleq1 2178 . 2 (𝐴 = 𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝐵 ∈ {𝑥𝜑}))
2 df-sbc 2881 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
3 df-sbc 2881 . 2 ([𝐵 / 𝑥]𝜑𝐵 ∈ {𝑥𝜑})
41, 2, 33bitr4g 222 1 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1314  wcel 1463  {cab 2101  [wsbc 2880
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111  df-sbc 2881
This theorem is referenced by:  sbceq1d  2885  sbc8g  2887  spsbc  2891  sbcco  2901  sbcco2  2902  sbcie2g  2912  elrabsf  2917  eqsbc3  2918  csbeq1  2976  sbcnestgf  3019  sbcco3g  3025  cbvralcsf  3030  cbvrexcsf  3031  findes  4485  ralrnmpt  5528  rexrnmpt  5529  findcard2  6749  findcard2s  6750  ac6sfi  6758  nn1suc  8699  uzind4s2  9338  indstr  9340  bezoutlemmain  11593  prmind2  11708
  Copyright terms: Public domain W3C validator