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

Theorem sdomnen 9002
Description: Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
sdomnen (𝐴𝐵 → ¬ 𝐴𝐵)

Proof of Theorem sdomnen
StepHypRef Expression
1 brsdom 8996 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
21simprbi 495 1 (𝐴𝐵 → ¬ 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   class class class wbr 5149  cen 8961  cdom 8962  csdm 8963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-br 5150  df-sdom 8967
This theorem is referenced by:  bren2  9004  domdifsn  9079  sucdom2OLD  9107  sdomnsym  9123  domnsym  9124  sdomirr  9139  domnsymfi  9228  sucdom2  9231  php5  9239  phpeqd  9240  phpeqdOLD  9250  1sdom2dom  9272  pssinf  9281  f1finf1o  9296  f1finf1oOLD  9297  isfinite2  9326  cardom  10011  pm54.43  10026  pr2neOLD  10030  alephdom  10106  cdainflem  10212  ackbij1b  10264  isfin4p1  10340  fin23lem25  10349  fin67  10420  axcclem  10482  canthp1lem2  10678  gchinf  10682  pwfseqlem4  10687  tskssel  10782  1nprm  16653  en2top  22932  domalom  37014  pibt2  37027  rp-isfinite6  43090  ensucne0OLD  43102  iscard5  43108  omiscard  43115
  Copyright terms: Public domain W3C validator