# Metamath Proof Explorer

## 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 {f}\phantom{\rule{.4em}{0ex}}{f}:{x}\underset{1-1 onto}{⟶}{y}\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cen ${class}\approx$
1 vx ${setvar}{x}$
2 vy ${setvar}{y}$
3 vf ${setvar}{f}$
4 3 cv ${setvar}{f}$
5 1 cv ${setvar}{x}$
6 2 cv ${setvar}{y}$
7 5 6 4 wf1o ${wff}{f}:{x}\underset{1-1 onto}{⟶}{y}$
8 7 3 wex ${wff}\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{x}\underset{1-1 onto}{⟶}{y}$
9 8 1 2 copab ${class}\left\{⟨{x},{y}⟩|\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{x}\underset{1-1 onto}{⟶}{y}\right\}$
10 0 9 wceq ${wff}\approx =\left\{⟨{x},{y}⟩|\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{x}\underset{1-1 onto}{⟶}{y}\right\}$