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	$$⊢\preccurlyeq =\left\{⟨x,y⟩|\exists ff:x\underset{1-1}{⟶}y\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdom	$$class\preccurlyeq$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3		vf	$$setvarf$$
4	3	cv	$$setvarf$$
5	1	cv	$$setvarx$$
6	2	cv	$$setvary$$
7	5 6 4	wf1	$$wfff:x\underset{1-1}{⟶}y$$
8	7 3	wex	$$wff\exists ff:x\underset{1-1}{⟶}y$$
9	8 1 2	copab	$$class\left\{⟨x,y⟩|\exists ff:x\underset{1-1}{⟶}y\right\}$$
10	0 9	wceq	$$wff\preccurlyeq =\left\{⟨x,y⟩|\exists ff:x\underset{1-1}{⟶}y\right\}$$