Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998) (Proof shortened by BTernaryTau, 23-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | bren | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | encv | |
|
2 | f1ofn | |
|
3 | fndm | |
|
4 | vex | |
|
5 | 4 | dmex | |
6 | 3 5 | eqeltrrdi | |
7 | 2 6 | syl | |
8 | f1ofo | |
|
9 | forn | |
|
10 | 8 9 | syl | |
11 | 4 | rnex | |
12 | 10 11 | eqeltrrdi | |
13 | 7 12 | jca | |
14 | 13 | exlimiv | |
15 | breng | |
|
16 | 1 14 15 | pm5.21nii | |