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

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2845, so we will allow direct use of df-sbc 2839. 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 2150 . 2 (𝐴 = 𝐵 → (𝐴 ∈ {𝑥𝜑} ↔ 𝐵 ∈ {𝑥𝜑}))
2 df-sbc 2839 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
3 df-sbc 2839 . 2 ([𝐵 / 𝑥]𝜑𝐵 ∈ {𝑥𝜑})
41, 2, 33bitr4g 221 1 (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑[𝐵 / 𝑥]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1289  wcel 1438  {cab 2074  [wsbc 2838
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-sbc 2839
This theorem is referenced by:  sbceq1d  2843  sbc8g  2845  spsbc  2849  sbcco  2859  sbcco2  2860  sbcie2g  2870  elrabsf  2875  eqsbc3  2876  csbeq1  2934  sbcnestgf  2977  sbcco3g  2983  cbvralcsf  2988  cbvrexcsf  2989  findes  4408  ralrnmpt  5425  rexrnmpt  5426  findcard2  6585  findcard2s  6586  ac6sfi  6594  nn1suc  8413  uzind4s2  9048  indstr  9050  bezoutlemmain  11080  prmind2  11195
  Copyright terms: Public domain W3C validator