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	$$⊢\approx =\left\{⟨x,y⟩|\exists ff:x\underset{1-1\; onto}{⟶}y\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cen	$$class\approx$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3		vf	$$setvarf$$
4	3	cv	$$setvarf$$
5	1	cv	$$setvarx$$
6	2	cv	$$setvary$$
7	5 6 4	wf1o	$$wfff:x\underset{1-1\; onto}{⟶}y$$
8	7 3	wex	$$wff\exists ff:x\underset{1-1\; onto}{⟶}y$$
9	8 1 2	copab	$$class\left\{⟨x,y⟩|\exists ff:x\underset{1-1\; onto}{⟶}y\right\}$$
10	0 9	wceq	$$wff\approx =\left\{⟨x,y⟩|\exists ff:x\underset{1-1\; onto}{⟶}y\right\}$$