Definition df-sbc 3717

Description: Define the proper substitution of a class for a set.

When 𝐴 is a proper class, our definition evaluates to false (see sbcex 3726). This is somewhat arbitrary: we could have, instead, chosen the conclusion of sbc6 3748 for our definition, whose right-hand side 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 3718 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 3718, which holds for both our definition and Quine's, and from which we can derive a weaker version of df-sbc 3717 in the form of sbc8g 3724. 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 3717 and assert that [𝐴 / 𝑥]𝜑 is always false when 𝐴 is a proper class.

Theorem sbc2or 3725 shows the apparently "strongest" statement we can make regarding behavior at proper classes if we start from dfsbcq 3718.

The related definition df-csb 3833 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 3716	. 2 wff [𝐴 / 𝑥]𝜑
5	1, 2	cab 2715	. . 3 class {𝑥 ∣ 𝜑}
6	3, 5	wcel 2106	. 2 wff 𝐴 ∈ {𝑥 ∣ 𝜑}
7	4, 6	wb 205	1 wff ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})

This definition is referenced by:  dfsbcq  3718  dfsbcq2  3719  sbceqbid  3723  sbcex  3726  nfsbc1d  3734  nfsbcdw  3737  nfsbcd  3740  sbc5  3744  sbc6g  3746  cbvsbcw  3750  cbvsbcvw  3751  cbvsbc  3752  sbcieg  3756  sbcied  3761  sbcbid  3774  sbcbi2  3778  sbcimdv  3790  sbcg  3795  intab  4909  brab1  5122  iotacl  6419  riotasbc  7251  scottexs  9645  scott0s  9646  hta  9655  issubc  17550  dmdprd  19601  sbceqbidf  30835  bnj1454  32822  bnj110  32838  setinds  33754  bj-csbsnlem  35088  rdgssun  35549  frege54cor1c  41523  frege55lem1c  41524  frege55c  41526