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 8551 | . 2 ⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) | |
2 | 1 | biimpi 218 | 1 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 class class class wbr 5058 ≈ cen 8500 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-opab 5121 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-er 8283 df-en 8504 |
This theorem is referenced by: ensymi 8553 ensymd 8554 sbthb 8632 domnsym 8637 sdomdomtr 8644 domsdomtr 8646 enen1 8651 enen2 8652 domen1 8653 domen2 8654 sdomen1 8655 sdomen2 8656 domtriord 8657 xpen 8674 pwen 8684 nneneq 8694 php2 8696 php3 8697 phpeqd 8700 ominf 8724 fineqvlem 8726 en1eqsn 8742 dif1en 8745 enp1i 8747 findcard3 8755 isfinite2 8770 nnsdomg 8771 domunfican 8785 infcntss 8786 fiint 8789 wdomen1 9034 wdomen2 9035 unxpwdom2 9046 karden 9318 finnum 9371 carden2b 9390 fidomtri2 9417 cardmin2 9421 pr2ne 9425 en2eleq 9428 infxpenlem 9433 acnen 9473 acnen2 9475 infpwfien 9482 alephordi 9494 alephinit 9515 dfac12lem2 9564 dfac12r 9566 undjudom 9587 djucomen 9597 djuinf 9608 pwsdompw 9620 infmap2 9634 ackbij1b 9655 cflim2 9679 fin4en1 9725 domfin4 9727 fin23lem25 9740 fin23lem23 9742 enfin1ai 9800 fin67 9811 isfin7-2 9812 fin1a2lem11 9826 axcc2lem 9852 axcclem 9873 numthcor 9910 carden 9967 sdomsdomcard 9976 canthnum 10065 canthwe 10067 canthp1lem2 10069 canthp1 10070 pwxpndom2 10081 gchdjuidm 10084 gchxpidm 10085 gchpwdom 10086 inawinalem 10105 grudomon 10233 isfinite4 13717 hashfn 13730 ramub2 16344 dfod2 18685 sylow2blem1 18739 znhash 20699 hauspwdom 22103 rectbntr0 23434 ovolctb 24085 dyadmbl 24195 eupthfi 27978 derangen 32414 finminlem 33661 domalom 34679 phpreu 34870 pellexlem4 39422 pellexlem5 39423 pellex 39425 |
Copyright terms: Public domain | W3C validator |