Definition df-clab 2151

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 2135, which extends or "overloads" the wel 2136 definition connecting setvar variables, requires that both sides of e. be a class. In df-cleq 2157 and df-clel 2160, 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 1341 allows us to substitute a setvar variable x for a class variable: all sets are classes by cvjust 2159 (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 2273 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 2273. (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 1341	. . 3 class x
3		wph	. . . 4 wff ph
4		vy	. . . 4 setvar y
5	3, 4	cab 2150	. . 3 class { y | ph }
6	2, 5	wcel 2135	. 2 wff x e. { y | ph }
7	3, 4, 1	wsb 1749	. 2 wff [ x / y ] ph
8	6, 7	wb 104	1 wff ( x e. { y | ph } <-> [ x / y ] ph )

This definition is referenced by:  abid  2152  hbab1  2153  hbab  2155  cvjust  2159  abbi  2278  sb8ab  2286  cbvabw  2287  cbvab  2288  clelab  2290  nfabdw  2325  nfabd  2326  vjust  2722  dfsbcq2  2949  sbc8g  2953  csbcow  3051  csbabg  3101  unab  3384  inab  3385  difab  3386  rabeq0  3433  abeq0  3434  oprcl  3776  exss  4199  peano1  4565  peano2  4566  iotaeq  5155  nfvres  5513  abrexex2g  6080  opabex3d  6081  opabex3  6082  abrexex2  6084  bdab  13555  bdph  13567  bdcriota  13600