Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sdomnen Unicode version

Theorem sdomnen 7564
 Description: Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
sdomnen

Proof of Theorem sdomnen
StepHypRef Expression
1 brsdom 7558 . 2
21simprbi 464 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4   class class class wbr 4452   cen 7533   cdom 7534   csdm 7535 This theorem is referenced by:  bren2  7566  domdifsn  7620  sdomnsym  7662  domnsym  7663  sdomirr  7674  php5  7725  sucdom2  7734  pssinf  7750  f1finf1o  7766  isfinite2  7798  cardom  8388  pm54.43  8402  pr2ne  8404  alephdom  8483  cdainflem  8592  ackbij1b  8640  isfin4-3  8716  fin23lem25  8725  fin67  8796  axcclem  8858  canthp1lem2  9052  gchinf  9056  pwfseqlem4  9061  tskssel  9156  1nprm  14222  en2top  19487  rp-isfinite6  37744 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-br 4453  df-sdom 7539
 Copyright terms: Public domain W3C validator