Definition df-sbc 3791

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

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

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

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

This definition is referenced by:  dfsbcq  3792  dfsbcq2  3793  sbceqbid  3797  sbcex  3800  nfsbc1d  3808  nfsbcdw  3811  nfsbcd  3814  sbc5  3818  sbc6g  3820  cbvsbcw  3824  cbvsbcvw  3825  cbvsbc  3826  sbcieg  3831  sbcied  3836  sbcbid  3849  sbcbi2  3853  sbcimdv  3864  sbcg  3869  intab  4982  brab1  5195  iotacl  6548  riotasbc  7405  scottexs  9924  scott0s  9925  hta  9934  issubc  17885  dmdprd  20032  sbceqbidf  32514  bnj1454  34834  bnj110  34850  setinds  35759  sbceqbii  36172  cbvsbcvw2  36212  cbvsbcdavw  36239  cbvsbcdavw2  36240  bj-csbsnlem  36885  rdgssun  37360  frege54cor1c  43904  frege55lem1c  43905  frege55c  43907