Definition df-dm 4788

Description: Define the domain of a class. The notation "dom " is used by Enderton; other authors sometimes use script D. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-dm	|- dom A = ran `'A

Detailed syntax breakdown of Definition df-dm

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cdm 4773	. 2 class dom A
3	1	ccnv 4772	. . 3 class `'A
4	3	crn 4774	. 2 class ran `'A
5	2, 4	wceq 1642	1 wff dom A = ran `'A

This definition is referenced by:  eldm  4899  nfdm  4965  rncoeq  4976  cnvimass  5017  cnvimarndm  5018  dminxp  5062  dmco  5090  cores2  5092  dmexg  5106  funimacnv  5169  foimacnv  5304  f1ococnv2  5310  fimacnv  5412  enprmaplem6  6082