Definition df-sbc 1441

Description: Define the proper substitution of a class for a set. This definition applies to proper classes but is not meaningful in that case (and does not produce the same results as Definition 6.6 of [Quine] p. 42). This definition is somewhat arbitrary - e.g., we could have used sbc6 1453 which yields a different result for proper classes. In order to allow for a possible alternate but conflicting definition in the future, we will use this definition only to prove dfsbcq 1442, which will then in turn serve as our "real" definition. Note: this definition extends or "overloads" df-sb 853 which ( via df-clab 1093) becomes a special case of it.

Theorem sbab 1188 shows how proper substitution into a class variable (as opposed to a wff) could be defined. (We do not have a separate notation for it at this time.)

Assertion

Ref	Expression
df-sbc	⊢ ([A / x]φ ↔ A ∈ {x∣φ})

Detailed syntax breakdown of Definition df-sbc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	wsbc 1440	. 2 wff [A / x]φ
5	1, 2	cab 1090	. . 3 class {x∣φ}
6	3, 5	wcel 1092	. 2 wff A ∈ {x∣φ}
7	4, 6	wb 127	1 wff ([A / x]φ ↔ A ∈ {x∣φ})

This definition is referenced by:  dfsbcq 1442

metamath.org