Definition df-clab 2162

Description: Define class abstraction notation (so-called by Quine), also called a "class builder" in the literature. x and y need not be distinct. Definition 2.1 of [Quine] p. 16. Typically, ph will have y as a free variable, and " { y | ph } " is read "the class of all sets y such that ph ( y ) is true". We do not define { y | ph } in isolation but only as part of an expression that extends or "overloads" the e. relationship.

This is our first use of the e. symbol to connect classes instead of sets. The syntax definition wcel 2146, which extends or "overloads" the wel 2147 definition connecting setvar variables, requires that both sides of e. be a class. In df-cleq 2168 and df-clel 2171, we introduce a new kind of variable (class variable) that can substituted with expressions such as { y | ph }. In the present definition, the x on the left-hand side is a setvar variable. Syntax definition cv 1352 allows us to substitute a setvar variable x for a class variable: all sets are classes by cvjust 2170 (but not necessarily vice-versa). For a full description of how classes are introduced and how to recover the primitive language, see the discussion in Quine (and under abeq2 2284 for a quick overview).

Because class variables can be substituted with compound expressions and setvar variables cannot, it is often useful to convert a theorem containing a free setvar variable to a more general version with a class variable.

This is called the "axiom of class comprehension" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. He calls the construction { y | ph } a "class term".

For a general discussion of the theory of classes, see https://us.metamath.org/mpeuni/mmset.html#class 2284. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Detailed syntax breakdown of Definition df-clab

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar x
2	1	cv 1352	. . 3 class x
3		wph	. . . 4 wff ph
4		vy	. . . 4 setvar y
5	3, 4	cab 2161	. . 3 class { y | ph }
6	2, 5	wcel 2146	. 2 wff x e. { y | ph }
7	3, 4, 1	wsb 1760	. 2 wff [ x / y ] ph
8	6, 7	wb 105	1 wff ( x e. { y | ph } <-> [ x / y ] ph )

This definition is referenced by:  abid  2163  hbab1  2164  hbab  2166  cvjust  2170  abbi  2289  sb8ab  2297  cbvabw  2298  cbvab  2299  clelab  2301  nfabdw  2336  nfabd  2337  vjust  2736  dfsbcq2  2963  sbc8g  2968  csbcow  3066  csbabg  3116  unab  3400  inab  3401  difab  3402  rabeq0  3450  abeq0  3451  oprcl  3798  exss  4221  peano1  4587  peano2  4588  iotaeq  5178  nfvres  5540  abrexex2g  6111  opabex3d  6112  opabex3  6113  abrexex2  6115  bdab  14130  bdph  14142  bdcriota  14175