| 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 8918 | . 2 ⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) | |
| 2 | 1 | biimpi 216 | 1 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 class class class wbr 5088 ≈ cen 8860 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5367 ax-un 7662 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ral 3045 df-rex 3054 df-rab 3393 df-v 3435 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-br 5089 df-opab 5151 df-id 5508 df-xp 5619 df-rel 5620 df-cnv 5621 df-co 5622 df-dm 5623 df-rn 5624 df-res 5625 df-ima 5626 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-er 8616 df-en 8864 |
| This theorem is referenced by: ensymi 8920 ensymd 8921 sbthb 9005 domnsym 9010 sdomdomtr 9017 domsdomtr 9019 enen1 9024 enen2 9025 domen1 9026 domen2 9027 sdomen1 9028 sdomen2 9029 domtriord 9030 xpen 9047 pwen 9057 fineqvlem 9144 dif1ennnALT 9155 isfinite2 9176 domunfican 9200 infcntss 9201 wdomen1 9456 wdomen2 9457 unxpwdom2 9468 karden 9779 finnum 9832 carden2b 9851 fidomtri2 9878 cardmin2 9883 en2eleq 9890 infxpenlem 9895 acnen 9935 acnen2 9937 infpwfien 9944 alephordi 9956 alephinit 9977 dfac12lem2 10027 dfac12r 10029 undjudom 10050 djucomen 10060 djuinf 10071 pwsdompw 10085 infmap2 10099 ackbij1b 10120 cflim2 10145 fin4en1 10191 domfin4 10193 fin23lem25 10206 fin23lem23 10208 enfin1ai 10266 fin67 10277 isfin7-2 10278 fin1a2lem11 10292 axcc2lem 10318 axcclem 10339 numthcor 10376 carden 10433 sdomsdomcard 10442 canthnum 10531 canthwe 10533 canthp1lem2 10535 canthp1 10536 pwxpndom2 10547 gchdjuidm 10550 gchxpidm 10551 gchpwdom 10552 inawinalem 10571 grudomon 10699 isfinite4 14257 hashfn 14270 ramub2 16913 dfod2 19430 sylow2blem1 19486 znhash 21449 hauspwdom 23370 rectbntr0 24702 ovolctb 25372 dyadmbl 25482 eupthfi 30136 derangen 35162 finminlem 36309 domalom 37395 phpreu 37601 pellexlem4 42822 pellexlem5 42823 pellex 42825 |
| Copyright terms: Public domain | W3C validator |