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

Theorem sdomnen 6975
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 6969 . 2  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
21simprbi 450 1  |-  ( A 
~<  B  ->  -.  A  ~~  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   class class class wbr 4102    ~~ cen 6945    ~<_ cdom 6946    ~< csdm 6947
This theorem is referenced by:  bren2  6977  domdifsn  7030  sdomnsym  7071  domnsym  7072  sdomirr  7083  php5  7134  sucdom2  7142  pssinf  7158  f1finf1o  7173  isfinite2  7202  cardom  7706  pm54.43  7720  pr2ne  7722  alephdom  7795  cdainflem  7904  ackbij1b  7952  isfin4-3  8028  fin23lem25  8037  fin67  8108  axcclem  8170  canthp1lem2  8362  gchinf  8366  pwfseqlem4  8371  tskssel  8466  1nprm  12854  en2top  16823
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-dif 3231  df-br 4103  df-sdom 6951
  Copyright terms: Public domain W3C validator