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 8561 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≈ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 5069 ≈ cen 8509 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ral 3146 df-rex 3147 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-br 5070 df-opab 5132 df-id 5463 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-er 8292 df-en 8513 |
This theorem is referenced by: entr2i 8567 entr3i 8568 entr4i 8569 pm54.43 9432 infxpenlem 9442 unsnen 9978 cfpwsdom 10009 tskinf 10194 inar1 10200 gruina 10243 uzenom 13335 znnen 15568 qnnen 15569 rexpen 15584 rucALT 15586 aleph1re 15601 aleph1irr 15602 unben 16248 1stcfb 22056 2ndcredom 22061 hauspwdom 22112 met1stc 23134 ovolctb2 24096 ovolfi 24098 ovoliunlem3 24108 uniiccdif 24182 dyadmbl 24204 mbfimaopnlem 24259 aannenlem3 24922 f1ocnt 30528 dmvlsiga 31392 sigapildsys 31425 omssubadd 31562 carsgclctunlem3 31582 pellex 39438 tr3dom 39900 nnfoctb 41315 nnf1oxpnn 41463 ioonct 41819 caragenunicl 42813 rrx2xpreen 44713 aacllem 44909 |
Copyright terms: Public domain | W3C validator |