# Metamath Proof Explorer

## Definition df-dm

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

Ref Expression
Assertion df-dm ${⊢}\mathrm{dom}{A}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 0 cdm ${class}\mathrm{dom}{A}$
2 vx ${setvar}{x}$
3 vy ${setvar}{y}$
4 2 cv ${setvar}{x}$
5 3 cv ${setvar}{y}$
6 4 5 0 wbr ${wff}{x}{A}{y}$
7 6 3 wex ${wff}\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
8 7 2 cab ${class}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}$
9 1 8 wceq ${wff}\mathrm{dom}{A}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}$