![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > enfi | Structured version Unicode version |
Description: Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.) |
Ref | Expression |
---|---|
enfi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enen1 7560 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rexbidv 2864 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | isfi 7442 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | isfi 7442 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4g 288 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-ral 2803 df-rex 2804 df-rab 2807 df-v 3078 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-op 3991 df-uni 4199 df-br 4400 df-opab 4458 df-id 4743 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-er 7210 df-en 7420 df-fin 7423 |
This theorem is referenced by: enfii 7640 wofib 7869 en2eleq 8285 sdom2en01 8581 fin23lem21 8618 enfin1ai 8663 fin17 8673 isfin7-2 8675 engch 8905 uzinf 11904 hasheni 12235 symggen 16094 psgnunilem1 16117 dfod2 16185 odhash 16193 gsumval3OLD 16502 gsumval3lem1 16503 gsumval3lem2 16504 gsumval3 16505 cyggic 18129 nbusgrafi 23508 cusgrafilem3 23540 eupai 23739 derangen 27203 erdsze2lem1 27234 diophin 29258 diophren 29299 fiphp3d 29305 fiuneneq 29709 |
Copyright terms: Public domain | W3C validator |