Definition df-dm 4850

Description: Define the domain of a class. Definition 3 of [Suppes] p. 59. For example, ={<.2,6>.,<.3,9>.}->dom={2,3} (ex-dm 23646). Another example is the domain of the complex arctangent, (for proof see atandm 22271). Contrast with range (defined in df-rn 4851). For alternate definitions see dfdm2 5369, dfdm3 5027, and dfdm4 5032. The notation "dom " is used by Enderton; other authors sometimes use script D. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-dm

Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-dm

Step	Hyp	Ref	Expression
1		cA	. . 3
2	1	cdm 4840	. 2
3		vx	. . . . . 6
4	3	cv 1368	. . . . 5
5		vy	. . . . . 6
6	5	cv 1368	. . . . 5
7	4, 6, 1	wbr 4292	. . . 4
8	7, 5	wex 1586	. . 3
9	8, 3	cab 2429	. 2
10	2, 9	wceq 1369	1

This definition is referenced by:  dfdm3  5027  dfrn2  5028  dfdm4  5032  dfdmf  5033  eldmg  5035  dmun  5046  dm0rn0  5056  nfdm  5081  fliftf  6008  opabdm  25943  domep  27606