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 8702 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≈ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 5069 ≈ cen 8646 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-sep 5208 ax-nul 5215 ax-pow 5274 ax-pr 5338 ax-un 7544 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3425 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4456 df-pw 4531 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4836 df-br 5070 df-opab 5132 df-id 5471 df-xp 5574 df-rel 5575 df-cnv 5576 df-co 5577 df-dm 5578 df-rn 5579 df-res 5580 df-ima 5581 df-fun 6402 df-fn 6403 df-f 6404 df-f1 6405 df-fo 6406 df-f1o 6407 df-er 8414 df-en 8650 |
This theorem is referenced by: entr2i 8708 entr3i 8709 entr4i 8710 pm54.43 9646 infxpenlem 9656 unsnen 10196 cfpwsdom 10227 tskinf 10412 inar1 10418 gruina 10461 uzenom 13568 znnen 15805 qnnen 15806 rexpen 15821 rucALT 15823 aleph1re 15838 aleph1irr 15839 unben 16494 1stcfb 22373 2ndcredom 22378 hauspwdom 22429 met1stc 23450 ovolctb2 24420 ovolfi 24422 ovoliunlem3 24432 uniiccdif 24506 dyadmbl 24528 mbfimaopnlem 24583 aannenlem3 25254 f1ocnt 30874 dmvlsiga 31840 sigapildsys 31873 omssubadd 32010 carsgclctunlem3 32030 pellex 40407 tr3dom 40867 nnfoctb 42315 nnf1oxpnn 42454 ioonct 42795 caragenunicl 43782 rrx2xpreen 45783 aacllem 46221 |
Copyright terms: Public domain | W3C validator |