![]() |
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 8380 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) | |
2 | 1 | simprbi 497 | 1 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 class class class wbr 4962 ≈ cen 8354 ≼ cdom 8355 ≺ csdm 8356 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-v 3439 df-dif 3862 df-br 4963 df-sdom 8360 |
This theorem is referenced by: bren2 8388 domdifsn 8447 sdomnsym 8489 domnsym 8490 sdomirr 8501 php5 8552 sucdom2 8560 pssinf 8574 f1finf1o 8591 isfinite2 8622 cardom 9261 pm54.43 9275 pr2ne 9277 alephdom 9353 cdainflem 9459 ackbij1b 9507 isfin4p1 9583 fin23lem25 9592 fin67 9663 axcclem 9725 canthp1lem2 9921 gchinf 9925 pwfseqlem4 9930 tskssel 10025 1nprm 15852 en2top 21277 domalom 34216 pibt2 34229 rp-isfinite6 39369 ensucne0OLD 39381 iscard5 39386 rr-php2d 40053 |
Copyright terms: Public domain | W3C validator |