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

Theorem sdomnen 7139
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 7133 . 2  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
21simprbi 452 1  |-  ( A 
~<  B  ->  -.  A  ~~  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   class class class wbr 4215    ~~ cen 7109    ~<_ cdom 7110    ~< csdm 7111
This theorem is referenced by:  bren2  7141  domdifsn  7194  sdomnsym  7235  domnsym  7236  sdomirr  7247  php5  7298  sucdom2  7306  pssinf  7322  f1finf1o  7338  isfinite2  7368  cardom  7878  pm54.43  7892  pr2ne  7894  alephdom  7967  cdainflem  8076  ackbij1b  8124  isfin4-3  8200  fin23lem25  8209  fin67  8280  axcclem  8342  canthp1lem2  8533  gchinf  8537  pwfseqlem4  8542  tskssel  8637  1nprm  13089  en2top  17055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-br 4216  df-sdom 7115
  Copyright terms: Public domain W3C validator