Definition df-sbc 1938

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 in how it behaves with proper classes - e.g., we could have used sbc6 1953, which yields a different result for proper classes. In order to allow for a possible alternate but conflicting definition in the future, we will not commit to any specific proper class behavior. Instead, we will use this definition only to prove dfsbcq 1939, which will in turn serve as the starting point for all theorems based on the definition. Note: this definition extends or "overloads" df-sb 1170 which (via df-clab 1462) becomes a special case of it, so a careful metalogical soundness justification, outside of Metamath, is needed for complete rigor; alternately, we could treat this definition as a new axiom.

The related definition df-csb 1998 defines proper substitution into a class variable (as opposed to a wff variable).

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 1168	. 2 wff [A / x]φ
5	1, 2	cab 1461	. . 3 class {x∣φ}
6	3, 5	wcel 956	. 2 wff A ∈ {x∣φ}
7	4, 6	wb 146	1 wff ([A / x]φ ↔ A ∈ {x∣φ})

This definition is referenced by:  dfsbcq 1939

Copyright terms: Public domain