Definition df-dm 4004

Description: Define the domain of a class. Definition 3 of [Suppes] p. 59. For alternate definitions see dfdm2 4421, dfdm3 4148, and dfdm4 4151. The notation "dom " is used by Enderton; other authors sometimes use script D.

Assertion

Ref	Expression
df-dm	|- dom A = {x | E.y xAy}

Distinct variable group:   x,y,A

Detailed syntax breakdown of Definition df-dm

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cdm 3986	. 2 class dom A
3		vx	. . . . . 6 set x
4	3	cv 1297	. . . . 5 class x
5		vy	. . . . . 6 set y
6	5	cv 1297	. . . . 5 class y
7	4, 6, 1	wbr 3338	. . . 4 wff xAy
8	7, 5	wex 1326	. . 3 wff E.y xAy
9	8, 3	cab 1871	. 2 class {x | E.y xAy}
10	2, 9	wceq 1298	1 wff dom A = {x | E.y xAy}

This definition is referenced by:  dfdm3 4148  dfrn2 4149  dfdm4 4151  eldm 4153  dmun 4163  dmiOLD 4173  dm0rn0 4175  dmcossOLD 4212  domep 13861  domleqt 15020

Copyright terms: Public domain