This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdom	$class ≼$
1		vx	$setvar x$
2		vy	$setvar y$
3		vf	$setvar f$
4	3	cv	$setvar f$
5	1	cv	$setvar x$
6	2	cv	$setvar y$
7	5 6 4	wf1	$wff f : x \underset{1-1}{⟶} y$
8	7 3	wex	$wff \exists f f : x \underset{1-1}{⟶} y$
9	8 1 2	copab	$class \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$
10	0 9	wceq	$wff ≼ = \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$