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

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

Proof of Theorem sdomnen
StepHypRef Expression
1 brsdom 8519 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
21simprbi 500 1 (𝐴𝐵 → ¬ 𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5033   ≈ cen 8493   ≼ cdom 8494   ≺ csdm 8495 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-dif 3887  df-br 5034  df-sdom 8499 This theorem is referenced by:  bren2  8527  domdifsn  8587  sucdom2  8614  sdomnsym  8630  domnsym  8631  sdomirr  8642  php5  8693  phpeqd  8694  pssinf  8716  f1finf1o  8733  isfinite2  8764  cardom  9403  pm54.43  9418  pr2ne  9420  alephdom  9496  cdainflem  9602  ackbij1b  9654  isfin4p1  9730  fin23lem25  9739  fin67  9810  axcclem  9872  canthp1lem2  10068  gchinf  10072  pwfseqlem4  10077  tskssel  10172  1nprm  16016  en2top  21593  domalom  34816  pibt2  34829  rp-isfinite6  40213  ensucne0OLD  40225  iscard5  40229
 Copyright terms: Public domain W3C validator