Definition df-en 5588

Description: Define the equinumerosity relation. Definition of [Enderton] p. 129. We define ~~ to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 5597.

Assertion

Ref	Expression
df-en	|- ~~ = {<.x, y>. | E.f f:x-1-1-onto->y}

Distinct variable group:   x,y,f

Detailed syntax breakdown of Definition df-en

Step	Hyp	Ref	Expression
1		cen 5584	. 2 class ~~
2		vx	. . . . . 6 set x
3	2	cv 1585	. . . . 5 class x
4		vy	. . . . . 6 set y
5	4	cv 1585	. . . . 5 class y
6		vf	. . . . . 6 set f
7	6	cv 1585	. . . . 5 class f
8	3, 5, 7	wf1o 4130	. . . 4 wff f:x-1-1-onto->y
9	8, 6	wex 1615	. . 3 wff E.f f:x-1-1-onto->y
10	9, 2, 4	copab 3565	. 2 class {<.x, y>. | E.f f:x-1-1-onto->y}
11	1, 10	wceq 1586	1 wff ~~ = {<.x, y>. | E.f f:x-1-1-onto->y}

This definition is referenced by:  relen 5592  breng 5595  enssdom 5603

Copyright terms: Public domain