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

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

However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 2765, so we will allow direct use of df-sbc 2759. 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 (A = B → ([A / x]φ[B / x]φ))

Proof of Theorem dfsbcq
StepHypRef Expression
1 eleq1 2097 . 2 (A = B → (A {xφ} ↔ B {xφ}))
2 df-sbc 2759 . 2 ([A / x]φA {xφ})
3 df-sbc 2759 . 2 ([B / x]φB {xφ})
41, 2, 33bitr4g 212 1 (A = B → ([A / x]φ[B / x]φ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1242   wcel 1390  {cab 2023  [wsbc 2758
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033  df-sbc 2759
This theorem is referenced by:  sbceq1d  2763  sbc8g  2765  spsbc  2769  sbcco  2779  sbcco2  2780  sbcie2g  2790  elrabsf  2795  eqsbc3  2796  csbeq1  2849  sbcnestgf  2891  sbcco3g  2897  cbvralcsf  2902  cbvrexcsf  2903  findes  4269  ralrnmpt  5252  rexrnmpt  5253  nn1suc  7674  uzind4s2  8270  indstr  8272
  Copyright terms: Public domain W3C validator