Definition df-sbc 1942

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 1957, 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 1943, which will in turn serve as the starting point for all theorems based on the definition. Note: this definition extends or "overloads" df-sb 1172 which (via df-clab 1464) 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 2002 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 1170	. 2 wff [A / x]ph
5	1, 2	cab 1463	. . 3 class {x | ph}
6	3, 5	wcel 958	. 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 1943

Copyright terms: Public domain