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

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

Proof of Theorem sdomnen
StepHypRef Expression
1 brsdom 7925 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
21simprbi 480 1 (𝐴𝐵 → ¬ 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   class class class wbr 4615  cen 7899  cdom 7900  csdm 7901
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3559  df-br 4616  df-sdom 7905
This theorem is referenced by:  bren2  7933  domdifsn  7990  sdomnsym  8032  domnsym  8033  sdomirr  8044  php5  8095  sucdom2  8103  pssinf  8117  f1finf1o  8134  isfinite2  8165  cardom  8759  pm54.43  8773  pr2ne  8775  alephdom  8851  cdainflem  8960  ackbij1b  9008  isfin4-3  9084  fin23lem25  9093  fin67  9164  axcclem  9226  canthp1lem2  9422  gchinf  9426  pwfseqlem4  9431  tskssel  9526  1nprm  15319  en2top  20703  rp-isfinite6  37366
  Copyright terms: Public domain W3C validator