Definition df-en 8968

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

Assertion

Ref	Expression
df-en	⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}

Distinct variable group:   𝑥,𝑦,𝑓

Detailed syntax breakdown of Definition df-en

Step	Hyp	Ref	Expression
1		cen 8964	. 2 class ≈
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1538	. . . . 5 class 𝑥
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1538	. . . . 5 class 𝑦
6		vf	. . . . . 6 setvar 𝑓
7	6	cv 1538	. . . . 5 class 𝑓
8	3, 5, 7	wf1o 6540	. . . 4 wff 𝑓:𝑥–1-1-onto→𝑦
9	8, 6	wex 1778	. . 3 wff ∃𝑓 𝑓:𝑥–1-1-onto→𝑦
10	9, 2, 4	copab 5185	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
11	1, 10	wceq 1539	1 wff ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}

This definition is referenced by:  relen  8972  breng  8976  enssdom  8999