| 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 8928 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≈ 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: class class class wbr 5092 ≈ cen 8869 |
| 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 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 |
| 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 3395 df-v 3438 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-br 5093 df-opab 5155 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-er 8625 df-en 8873 |
| This theorem is referenced by: entr2i 8934 entr3i 8935 entr4i 8936 pm54.43 9897 infxpenlem 9907 unsnen 10447 cfpwsdom 10478 tskinf 10663 inar1 10669 gruina 10712 uzenom 13871 znnen 16121 qnnen 16122 rexpen 16137 rucALT 16139 aleph1re 16154 aleph1irr 16155 unben 16821 1stcfb 23330 2ndcredom 23335 hauspwdom 23386 met1stc 24407 ovolctb2 25391 ovolfi 25393 ovoliunlem3 25403 uniiccdif 25477 dyadmbl 25499 mbfimaopnlem 25554 aannenlem3 26236 f1ocnt 32746 dmvlsiga 34102 sigapildsys 34135 omssubadd 34274 carsgclctunlem3 34294 pellex 42818 tr3dom 43511 nnfoctb 45036 nnf1oxpnn 45183 ioonct 45528 caragenunicl 46515 rrx2xpreen 48714 aacllem 49796 |
| Copyright terms: Public domain | W3C validator |