| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ensymi | Structured version Visualization version GIF version | ||
| Description: Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.) |
| Ref | Expression |
|---|---|
| ensymi.2 | ⊢ 𝐴 ≈ 𝐵 |
| Ref | Expression |
|---|---|
| ensymi | ⊢ 𝐵 ≈ 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ensymi.2 | . 2 ⊢ 𝐴 ≈ 𝐵 | |
| 2 | ensym 8940 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≈ 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: 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: entr2i 8946 entr3i 8947 entr4i 8948 pm54.43 9913 infxpenlem 9923 unsnen 10463 cfpwsdom 10495 tskinf 10680 inar1 10686 gruina 10729 uzenom 13887 znnen 16137 qnnen 16138 rexpen 16153 rucALT 16155 aleph1re 16170 aleph1irr 16171 unben 16837 ex-chn2 18561 1stcfb 23389 2ndcredom 23394 hauspwdom 23445 met1stc 24465 ovolctb2 25449 ovolfi 25451 ovoliunlem3 25461 uniiccdif 25535 dyadmbl 25557 mbfimaopnlem 25612 aannenlem3 26294 f1ocnt 32880 dmvlsiga 34286 sigapildsys 34319 omssubadd 34457 carsgclctunlem3 34477 pellex 43073 tr3dom 43765 nnfoctb 45289 nnf1oxpnn 45435 ioonct 45779 caragenunicl 46764 rrx2xpreen 48961 aacllem 50042 |
| Copyright terms: Public domain | W3C validator |