Definition df-en

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 . (Contributed by NM, 28-Mar-1998)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cen	|- ~~
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	wf1o	|- f : x -1-1-onto-> y
8	7 3	wex	|- E. f f : x -1-1-onto-> y
9	8 1 2	copab	|- { <. x , y >. | E. f f : x -1-1-onto-> y }
10	0 9	wceq	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }