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

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

Proof of Theorem sdomnen
StepHypRef Expression
1 brsdom 8380 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
21simprbi 497 1 (𝐴𝐵 → ¬ 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   class class class wbr 4962  cen 8354  cdom 8355  csdm 8356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-dif 3862  df-br 4963  df-sdom 8360
This theorem is referenced by:  bren2  8388  domdifsn  8447  sdomnsym  8489  domnsym  8490  sdomirr  8501  php5  8552  sucdom2  8560  pssinf  8574  f1finf1o  8591  isfinite2  8622  cardom  9261  pm54.43  9275  pr2ne  9277  alephdom  9353  cdainflem  9459  ackbij1b  9507  isfin4p1  9583  fin23lem25  9592  fin67  9663  axcclem  9725  canthp1lem2  9921  gchinf  9925  pwfseqlem4  9930  tskssel  10025  1nprm  15852  en2top  21277  domalom  34216  pibt2  34229  rp-isfinite6  39369  ensucne0OLD  39381  iscard5  39386  rr-php2d  40053
  Copyright terms: Public domain W3C validator