# Metamath Proof Explorer

## Theorem bren

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998)

Ref Expression
Assertion bren ${⊢}{A}\approx {B}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}$

### Proof

Step Hyp Ref Expression
1 encv ${⊢}{A}\approx {B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
2 f1ofn ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}Fn{A}$
3 fndm ${⊢}{f}Fn{A}\to \mathrm{dom}{f}={A}$
4 vex ${⊢}{f}\in \mathrm{V}$
5 4 dmex ${⊢}\mathrm{dom}{f}\in \mathrm{V}$
6 3 5 eqeltrrdi ${⊢}{f}Fn{A}\to {A}\in \mathrm{V}$
7 2 6 syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {A}\in \mathrm{V}$
8 f1ofo ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}:{A}\underset{onto}{⟶}{B}$
9 forn ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \mathrm{ran}{f}={B}$
10 8 9 syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \mathrm{ran}{f}={B}$
11 4 rnex ${⊢}\mathrm{ran}{f}\in \mathrm{V}$
12 10 11 eqeltrrdi ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {B}\in \mathrm{V}$
13 7 12 jca ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
14 13 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
15 f1oeq2 ${⊢}{x}={A}\to \left({f}:{x}\underset{1-1 onto}{⟶}{y}↔{f}:{A}\underset{1-1 onto}{⟶}{y}\right)$
16 15 exbidv ${⊢}{x}={A}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{x}\underset{1-1 onto}{⟶}{y}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{y}\right)$
17 f1oeq3 ${⊢}{y}={B}\to \left({f}:{A}\underset{1-1 onto}{⟶}{y}↔{f}:{A}\underset{1-1 onto}{⟶}{B}\right)$
18 17 exbidv ${⊢}{y}={B}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{y}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}\right)$
19 df-en ${⊢}\approx =\left\{⟨{x},{y}⟩|\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{x}\underset{1-1 onto}{⟶}{y}\right\}$
20 16 18 19 brabg ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to \left({A}\approx {B}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}\right)$
21 1 14 20 pm5.21nii ${⊢}{A}\approx {B}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}$