Definition df-clab 2183

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 2167, which extends or "overloads" the wel 2168 definition connecting setvar variables, requires that both sides of e. be a class. In df-cleq 2189 and df-clel 2192, 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 1363 allows us to substitute a setvar variable x for a class variable: all sets are classes by cvjust 2191 (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 2305 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 2305. (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 1363	. . 3 class x
3		wph	. . . 4 wff ph
4		vy	. . . 4 setvar y
5	3, 4	cab 2182	. . 3 class { y | ph }
6	2, 5	wcel 2167	. 2 wff x e. { y | ph }
7	3, 4, 1	wsb 1776	. 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  2184  hbab1  2185  hbab  2187  cvjust  2191  abbi  2310  sb8ab  2318  cbvabw  2319  cbvab  2320  clelab  2322  eqabdv  2325  nfabdw  2358  nfabd  2359  vjust  2764  dfsbcq2  2992  sbc8g  2997  csbcow  3095  csbabg  3146  unab  3431  inab  3432  difab  3433  rabeq0  3481  abeq0  3482  oprcl  3833  exss  4261  peano1  4631  peano2  4632  iotaeq  5228  nfvres  5595  abrexex2g  6186  opabex3d  6187  opabex3  6188  abrexex2  6190  bdab  15568  bdph  15580  bdcriota  15613