Definition df-en 3274

Description: Define equinumerosity relation. Definition of [Enderton] p. 129, except we consider ≈ to be a (proper) class rather than a connective. This is acceptable because equinumerosity is meaningful for sets only and not for proper classes. (Well, some authors do consider it for proper classes: it turns out that all proper classes are equinumerous to the universe V, which is interesting and somewhat deep, but we will not need that result.) We derive the usual definition as bren 3282.

Assertion

Ref	Expression
df-en	⊢ ≈ = {⟨x, y⟩∣∃f f:x–1-1-onto→y}

Distinct variable group(s):   x,y,f

Detailed syntax breakdown of Definition df-en

Step	Hyp	Ref	Expression
1		cen 3271	. 2 class ≈
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		vy	. . . . . 6 set y
5	4	cv 1089	. . . . 5 class y
6		vf	. . . . . 6 set f
7	6	cv 1089	. . . . 5 class f
8	3, 5, 7	wf1o 2421	. . . 4 wff f:x–1-1-onto→y
9	8, 6	wex 678	. . 3 wff ∃f f:x–1-1-onto→y
10	9, 2, 4	copab 2055	. 2 class {⟨x, y⟩∣∃f f:x–1-1-onto→y}
11	1, 10	wceq 1091	1 wff ≈ = {⟨x, y⟩∣∃f f:x–1-1-onto→y}

This definition is referenced by:  relen 3277  breng 3280  enssdom 3287

metamath.org