Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dm Unicode version

Definition df-dm 4872
 Description: Define the domain of a class. Definition 3 of [Suppes] p. 59. For example, ={<.2,6>.,<.3,9>.}->dom ={2,3} (ex-dm 22768). Another example is the domain of the complex arctangent, (for proof see atandm 21737). Contrast with range (defined in df-rn 4873). For alternate definitions see dfdm2 5389, dfdm3 5049, and dfdm4 5054. 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
StepHypRef Expression
1 cA . . 3
21cdm 4862 . 2
3 vx . . . . . 6
43cv 1669 . . . . 5
5 vy . . . . . 6
65cv 1669 . . . . 5
74, 6, 1wbr 4318 . . . 4
87, 5wex 1565 . . 3
98, 3cab 2475 . 2
102, 9wceq 1670 1
 Colors of variables: wff set class This definition is referenced by:  dfdm3  5049  dfrn2  5050  dfdm4  5054  dfdmf  5055  eldmg  5057  dmun  5068  dm0rn0  5078  nfdm  5103  fliftf  6018  opabdm  25070  domep  26759
 Copyright terms: Public domain W3C validator