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

Theorem sdomnen 7338
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 7332 . 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 4292    ~~ cen 7307    ~<_ cdom 7308    ~< csdm 7309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-dif 3331  df-br 4293  df-sdom 7313
This theorem is referenced by:  bren2  7340  domdifsn  7394  sdomnsym  7436  domnsym  7437  sdomirr  7448  php5  7499  sucdom2  7507  pssinf  7523  f1finf1o  7539  isfinite2  7570  cardom  8156  pm54.43  8170  pr2ne  8172  alephdom  8251  cdainflem  8360  ackbij1b  8408  isfin4-3  8484  fin23lem25  8493  fin67  8564  axcclem  8626  canthp1lem2  8820  gchinf  8824  pwfseqlem4  8829  tskssel  8924  1nprm  13768  en2top  18590
  Copyright terms: Public domain W3C validator