Definition df-sbc 3742

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

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

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

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

This definition is referenced by:  dfsbcq  3743  dfsbcq2  3744  sbceqbid  3748  sbcex  3751  nfsbc1d  3759  nfsbcdw  3762  nfsbcd  3765  sbc5  3769  sbc6g  3771  cbvsbcw  3774  cbvsbcvw  3775  cbvsbc  3776  sbcieg  3781  sbcied  3785  sbcbid  3796  sbcbi2  3800  sbcimdv  3810  sbcg  3814  intab  4934  brab1  5147  iotacl  6479  riotasbc  7335  setinds  9662  scottexs  9803  scott0s  9804  hta  9813  issubc  17763  dmdprd  19933  sbceqbidf  32564  bnj1454  35000  bnj110  35016  sbceqbii  36387  cbvsbcvw2  36426  cbvsbcdavw  36453  cbvsbcdavw2  36454  bj-csbsnlem  37106  rdgssun  37585  frege54cor1c  44223  frege55lem1c  44224  frege55c  44226