Definition df-sbc 3789

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

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

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

The related definition df-csb 3900 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 3788	. 2 wff [𝐴 / 𝑥]𝜑
5	1, 2	cab 2714	. . 3 class {𝑥 ∣ 𝜑}
6	3, 5	wcel 2108	. 2 wff 𝐴 ∈ {𝑥 ∣ 𝜑}
7	4, 6	wb 206	1 wff ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})

This definition is referenced by:  dfsbcq  3790  dfsbcq2  3791  sbceqbid  3795  sbcex  3798  nfsbc1d  3806  nfsbcdw  3809  nfsbcd  3812  sbc5  3816  sbc6g  3818  cbvsbcw  3821  cbvsbcvw  3822  cbvsbc  3823  sbcieg  3828  sbcied  3832  sbcbid  3844  sbcbi2  3848  sbcimdv  3859  sbcg  3863  intab  4978  brab1  5191  iotacl  6547  riotasbc  7406  scottexs  9927  scott0s  9928  hta  9937  issubc  17880  dmdprd  20018  sbceqbidf  32506  bnj1454  34856  bnj110  34872  setinds  35779  sbceqbii  36192  cbvsbcvw2  36231  cbvsbcdavw  36258  cbvsbcdavw2  36259  bj-csbsnlem  36904  rdgssun  37379  frege54cor1c  43928  frege55lem1c  43929  frege55c  43931