MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sbc Unicode version

Definition df-sbc 3298
Description: Define the proper substitution of a class for a set.

When is a proper class, our definition evaluates to false. This is somewhat arbitrary: we could have, instead, chosen the conclusion of sbc6 3324 for our definition, which always evaluates to true for proper classes.

Our definition also does not produce the same results as discussed in the proof of Theorem 6.6 of [Quine] p. 42 (although Theorem 6.6 itself does hold, as shown by dfsbcq 3299 below). For example, if is a proper class, Quine's substitution of for in evaluates to rather than our falsehood. (This can be seen by substituting , , and for alpha, beta, and gamma in Subcase 1 of Quine's discussion on p. 42.) Unfortunately, Quine's definition requires a recursive syntactical breakdown of , and it does not seem possible to express it with a single closed formula.

If we did not want to commit to any specific proper class behavior, we could use this definition only to prove theorem dfsbcq 3299, which holds for both our definition and Quine's, and from which we can derive a weaker version of df-sbc 3298 in the form of sbc8g 3305. However, the behavior of Quine's definition at proper classes is similarly arbitrary, and for practical reasons (to avoid having to prove sethood of in every use of this definition) we allow direct reference to df-sbc 3298 and assert that is always false when is a proper class.

The theorem sbc2or 3306 shows the apparently "strongest" statement we can make regarding behavior at proper classes if we start from dfsbcq 3299.

The related definition df-csb 3402 defines proper substitution into a class variable (as opposed to a wff variable). (Contributed by NM, 14-Apr-1995.) (Revised by NM, 25-Dec-2016.)

Ref Expression

Detailed syntax breakdown of Definition df-sbc
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 cA . . 3
41, 2, 3wsbc 3297 . 2
51, 2cab 2439 . . 3
63, 5wcel 1758 . 2
74, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  dfsbcq  3299  dfsbcq2  3300  sbceqbid  3304  sbcex  3307  nfsbc1d  3315  nfsbcd  3318  cbvsbc  3326  sbcbi2  3348  sbcbid  3355  intab  4275  brab1  4454  iotacl  5523  riotasbc  6199  scottexs  8231  scott0s  8232  hta  8241  issubc  14907  dmdprd  16655  sbceqbidf  26334  setinds  28047  bnj1454  32678  bnj110  32694  bj-csbsnlem  33250  frege54cor1c  36596  frege55lem1c  36597  frege55c  36599  frege58newc  36602
  Copyright terms: Public domain W3C validator