Definition df-sbc 3403

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 3429 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 3404 below). For example, if 𝐴 is a proper class, Quine's substitution of 𝐴 for 𝑦 in 0 ∈ 𝑦 evaluates to 0 ∈ 𝐴 rather than our falsehood. (This can be seen by substituting 𝐴, 𝑦, and 0 for alpha, beta, and gamma in Subcase 1 of Quine's discussion on p. 42.) Unfortunately, Quine's definition requires a recursive syntactic 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 3404, which holds for both our definition and Quine's, and from which we can derive a weaker version of df-sbc 3403 in the form of sbc8g 3410. 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 3403 and assert that [𝐴 / 𝑥]𝜑 is always false when 𝐴 is a proper class.

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

The related definition df-csb 3500 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.)

Assertion

Ref	Expression
df-sbc	⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})

Detailed syntax breakdown of Definition df-sbc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wsbc 3402	. 2 wff [𝐴 / 𝑥]𝜑
5	1, 2	cab 2596	. . 3 class {𝑥 ∣ 𝜑}
6	3, 5	wcel 1977	. 2 wff 𝐴 ∈ {𝑥 ∣ 𝜑}
7	4, 6	wb 195	1 wff ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})

This definition is referenced by:  dfsbcq  3404  dfsbcq2  3405  sbceqbid  3409  sbcex  3412  nfsbc1d  3420  nfsbcd  3423  cbvsbc  3431  sbcbi2  3451  sbcbid  3456  intab  4442  brab1  4630  iotacl  5791  riotasbc  6526  scottexs  8633  scott0s  8634  hta  8643  issubc  16318  dmdprd  18220  sbceqbidf  28705  bnj1454  30166  bnj110  30182  setinds  30927  bj-csbsnlem  32090  frege54cor1c  37229  frege55lem1c  37230  frege55c  37232