![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > enfi | Structured version Visualization version GIF version |
Description: Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.) |
Ref | Expression |
---|---|
enfi | ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enen1 8509 | . . 3 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ 𝑥 ↔ 𝐵 ≈ 𝑥)) | |
2 | 1 | rexbidv 3260 | . 2 ⊢ (𝐴 ≈ 𝐵 → (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ↔ ∃𝑥 ∈ ω 𝐵 ≈ 𝑥)) |
3 | isfi 8386 | . 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) | |
4 | isfi 8386 | . 2 ⊢ (𝐵 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐵 ≈ 𝑥) | |
5 | 2, 3, 4 | 3bitr4g 315 | 1 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∈ wcel 2081 ∃wrex 3106 class class class wbr 4966 ωcom 7441 ≈ cen 8359 Fincfn 8362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-er 8144 df-en 8363 df-fin 8366 |
This theorem is referenced by: enfii 8586 wofib 8860 en2eleq 9285 sdom2en01 9575 fin23lem21 9612 enfin1ai 9657 fin17 9667 isfin7-2 9669 engch 9901 uzinf 13188 hasheni 13563 isfinite4 13578 symggen 18334 psgnunilem1 18357 dfod2 18426 odhash 18434 gsumval3lem2 18752 gsumval3 18753 cyggic 20406 cusgrfilem3 26927 unidifsnel 29989 unidifsnne 29990 derangen 32034 erdsze2lem1 32065 phpreu 34433 lindsdom 34443 poimirlem30 34479 diophin 38880 diophren 38921 fiphp3d 38927 fiuneneq 39308 |
Copyright terms: Public domain | W3C validator |