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

Theorem sdomnen 7545
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 7539 . 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 4447    ~~ cen 7514    ~<_ cdom 7515    ~< csdm 7516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-br 4448  df-sdom 7520
This theorem is referenced by:  bren2  7547  domdifsn  7601  sdomnsym  7643  domnsym  7644  sdomirr  7655  php5  7706  sucdom2  7715  pssinf  7731  f1finf1o  7747  isfinite2  7779  cardom  8368  pm54.43  8382  pr2ne  8384  alephdom  8463  cdainflem  8572  ackbij1b  8620  isfin4-3  8696  fin23lem25  8705  fin67  8776  axcclem  8838  canthp1lem2  9032  gchinf  9036  pwfseqlem4  9041  tskssel  9136  1nprm  14084  en2top  19293
  Copyright terms: Public domain W3C validator