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

Theorem sdomnen 7543
Description: Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
sdomnen  |-  ( A 
~<  B  ->  -.  A  ~~  B )

Proof of Theorem sdomnen
StepHypRef Expression
1 brsdom 7537 . 2  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
21simprbi 464 1  |-  ( A 
~<  B  ->  -.  A  ~~  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   class class class wbr 4434    ~~ cen 7512    ~<_ cdom 7513    ~< csdm 7514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-dif 3462  df-br 4435  df-sdom 7518
This theorem is referenced by:  bren2  7545  domdifsn  7599  sdomnsym  7641  domnsym  7642  sdomirr  7653  php5  7704  sucdom2  7713  pssinf  7729  f1finf1o  7745  isfinite2  7777  cardom  8367  pm54.43  8381  pr2ne  8383  alephdom  8462  cdainflem  8571  ackbij1b  8619  isfin4-3  8695  fin23lem25  8704  fin67  8775  axcclem  8837  canthp1lem2  9031  gchinf  9035  pwfseqlem4  9040  tskssel  9135  1nprm  14096  en2top  19357  rp-isfinite6  37430
  Copyright terms: Public domain W3C validator