Definition df-sbc 1913

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 1928, 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 1914, which will in turn serve as the starting point for all theorems based on the definition. Note: this definition extends or "overloads" df-sb 1155 which (via df-clab 1441) 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 1973 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 1153	. 2 wff [A / x]ph
5	1, 2	cab 1440	. . 3 class {x | ph}
6	3, 5	wcel 1105	. 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 1914

Copyright terms: Public domain