| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ensym | Structured version Visualization version GIF version | ||
| Description: Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
| Ref | Expression |
|---|---|
| ensym | ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ensymb 8939 | . 2 ⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) | |
| 2 | 1 | biimpi 216 | 1 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 class class class wbr 5098 ≈ cen 8880 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-er 8635 df-en 8884 |
| This theorem is referenced by: ensymi 8941 ensymd 8942 sbthb 9026 domnsym 9031 sdomdomtr 9038 domsdomtr 9040 enen1 9045 enen2 9046 domen1 9047 domen2 9048 sdomen1 9049 sdomen2 9050 domtriord 9051 xpen 9068 pwen 9078 fineqvlem 9166 dif1ennnALT 9177 isfinite2 9198 domunfican 9222 infcntss 9223 wdomen1 9481 wdomen2 9482 unxpwdom2 9493 karden 9807 finnum 9860 carden2b 9879 fidomtri2 9906 cardmin2 9911 en2eleq 9918 infxpenlem 9923 acnen 9963 acnen2 9965 infpwfien 9972 alephordi 9984 alephinit 10005 dfac12lem2 10055 dfac12r 10057 undjudom 10078 djucomen 10088 djuinf 10099 pwsdompw 10113 infmap2 10127 ackbij1b 10148 cflim2 10173 fin4en1 10219 domfin4 10221 fin23lem25 10234 fin23lem23 10236 enfin1ai 10294 fin67 10305 isfin7-2 10306 fin1a2lem11 10320 axcc2lem 10346 axcclem 10367 numthcor 10404 carden 10461 sdomsdomcard 10470 canthnum 10560 canthwe 10562 canthp1lem2 10564 canthp1 10565 pwxpndom2 10576 gchdjuidm 10579 gchxpidm 10580 gchpwdom 10581 inawinalem 10600 grudomon 10728 isfinite4 14285 hashfn 14298 ramub2 16942 dfod2 19493 sylow2blem1 19549 znhash 21513 hauspwdom 23445 rectbntr0 24777 ovolctb 25447 dyadmbl 25557 eupthfi 30280 derangen 35366 finminlem 36512 domalom 37605 phpreu 37801 pellexlem4 43070 pellexlem5 43071 pellex 43073 |
| Copyright terms: Public domain | W3C validator |