|   | 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 9016 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) | |
| 2 | 1 | simprbi 496 | 1 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 class class class wbr 5142 ≈ cen 8983 ≼ cdom 8984 ≺ csdm 8985 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-dif 3953 df-br 5143 df-sdom 8989 | 
| This theorem is referenced by: bren2 9024 domdifsn 9095 sucdom2OLD 9123 sdomnsym 9139 domnsym 9140 sdomirr 9155 domnsymfi 9241 sucdom2 9244 php5 9252 phpeqd 9253 phpeqdOLD 9263 1sdom2dom 9284 pssinf 9293 f1finf1o 9306 f1finf1oOLD 9307 isfinite2 9335 cardom 10027 pm54.43 10042 pr2neOLD 10046 alephdom 10122 cdainflem 10229 ackbij1b 10279 isfin4p1 10356 fin23lem25 10365 fin67 10436 axcclem 10498 canthp1lem2 10694 gchinf 10698 pwfseqlem4 10703 tskssel 10798 1nprm 16717 en2top 22993 domalom 37406 pibt2 37419 rp-isfinite6 43536 ensucne0OLD 43548 iscard5 43554 omiscard 43561 | 
| Copyright terms: Public domain | W3C validator |