Theorem sdomnen 7564

Description: Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)

Assertion

Ref	Expression
sdomnen

Proof of Theorem sdomnen

Step	Hyp	Ref	Expression
1		brsdom 7558	. 2
2	1	simprbi 464	1

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