Definition df-sbc 1939

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 1954, 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 1940, which will in turn serve as the starting point for all theorems based on the definition. Note: this definition extends or "overloads" df-sb 1171 which (via df-clab 1463) 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 1999 defines proper substitution into a class variable (as opposed to a wff variable).

Assertion

Ref	Expression
df-sbc	|- ([A / x]ph <-> A e. {x | ph})

Detailed syntax breakdown of Definition df-sbc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	wsbc 1169	. 2 wff [A / x]ph
5	1, 2	cab 1462	. . 3 class {x | ph}
6	3, 5	wcel 957	. 2 wff A e. {x | ph}
7	4, 6	wb 146	1 wff ([A / x]ph <-> A e. {x | ph})

This definition is referenced by:  dfsbcq 1940

Copyright terms: Public domain