Definition df-dom

Description: Define the dominance relation. For an alternate definition see dfdom2 . Compare Definition of Enderton p. 145. Typical textbook definitions are derived as brdom and domen . (Contributed by NM, 28-Mar-1998)

	Ref	Expression
Assertion	df-dom	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdom	|- ~<_
1		vx	|- x
2		vy	|- y
3		vf	|- f
4	3	cv	|- f
5	1	cv	|- x
6	2	cv	|- y
7	5 6 4	wf1	|- f : x -1-1-> y
8	7 3	wex	|- E. f f : x -1-1-> y
9	8 1 2	copab	|- { <. x , y >. | E. f f : x -1-1-> y }
10	0 9	wceq	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }