![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sdomnen | Structured version Visualization version GIF version |
Description: Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.) |
Ref | Expression |
---|---|
sdomnen | ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brsdom 8996 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) | |
2 | 1 | simprbi 495 | 1 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 class class class wbr 5149 ≈ cen 8961 ≼ cdom 8962 ≺ csdm 8963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-dif 3947 df-br 5150 df-sdom 8967 |
This theorem is referenced by: bren2 9004 domdifsn 9079 sucdom2OLD 9107 sdomnsym 9123 domnsym 9124 sdomirr 9139 domnsymfi 9228 sucdom2 9231 php5 9239 phpeqd 9240 phpeqdOLD 9250 1sdom2dom 9272 pssinf 9281 f1finf1o 9296 f1finf1oOLD 9297 isfinite2 9326 cardom 10011 pm54.43 10026 pr2neOLD 10030 alephdom 10106 cdainflem 10212 ackbij1b 10264 isfin4p1 10340 fin23lem25 10349 fin67 10420 axcclem 10482 canthp1lem2 10678 gchinf 10682 pwfseqlem4 10687 tskssel 10782 1nprm 16653 en2top 22932 domalom 37014 pibt2 37027 rp-isfinite6 43090 ensucne0OLD 43102 iscard5 43108 omiscard 43115 |
Copyright terms: Public domain | W3C validator |