HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-dm 3183
Description: Define the domain of a class. Definition 3 of [Suppes] p. 59.
Assertion
Ref Expression
df-dm |- dom A = {x | E.y xAy}
Distinct variable group:   x,y,A
Detailed syntax breakdown of Definition df-dm
StepHypRef Expression
1 cA . . 3 class A
21cdm 3165 . 2 class dom A
3 vx . . . . . 6 set x
43cv 953 . . . . 5 class x
5 vy . . . . . 6 set y
65cv 953 . . . . 5 class y
74, 6, 1wbr 2614 . . . 4 wff xAy
87, 5wex 978 . . 3 wff E.y xAy
98, 3cab 1461 . 2 class {x | E.y xAy}
102, 9wceq 954 1 wff dom A = {x | E.y xAy}
Colors of variables: wff set class
This definition is referenced by:  dfdm3 3297  dfrn2 3298  dfdm4 3300  eldm 3302  dmi 3321  dm0rn0 3325  dmcoss 3355
Copyright terms: Public domain