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

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

Proof of Theorem sdomnen
StepHypRef Expression
1 brsdom 7938 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
21simprbi 480 1 (𝐴𝐵 → ¬ 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   class class class wbr 4623  cen 7912  cdom 7913  csdm 7914
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 3192  df-dif 3563  df-br 4624  df-sdom 7918
This theorem is referenced by:  bren2  7946  domdifsn  8003  sdomnsym  8045  domnsym  8046  sdomirr  8057  php5  8108  sucdom2  8116  pssinf  8130  f1finf1o  8147  isfinite2  8178  cardom  8772  pm54.43  8786  pr2ne  8788  alephdom  8864  cdainflem  8973  ackbij1b  9021  isfin4-3  9097  fin23lem25  9106  fin67  9177  axcclem  9239  canthp1lem2  9435  gchinf  9439  pwfseqlem4  9444  tskssel  9539  1nprm  15335  en2top  20729  rp-isfinite6  37384
  Copyright terms: Public domain W3C validator