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 | f f : x 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 1-1 y
8 7 3 wex wff f f : x 1-1 y
9 8 1 2 copab class x y | f f : x 1-1 y
10 0 9 wceq wff = x y | f f : x 1-1 y