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

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

Proof of Theorem sdomnen
StepHypRef Expression
1 brsdom 8973 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
21simprbi 495 1 (𝐴𝐵 → ¬ 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   class class class wbr 5147  cen 8938  cdom 8939  csdm 8940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950  df-br 5148  df-sdom 8944
This theorem is referenced by:  bren2  8981  domdifsn  9056  sucdom2OLD  9084  sdomnsym  9100  domnsym  9101  sdomirr  9116  domnsymfi  9205  sucdom2  9208  php5  9216  phpeqd  9217  phpeqdOLD  9227  1sdom2dom  9249  pssinf  9258  f1finf1o  9273  f1finf1oOLD  9274  isfinite2  9303  cardom  9983  pm54.43  9998  pr2neOLD  10002  alephdom  10078  cdainflem  10184  ackbij1b  10236  isfin4p1  10312  fin23lem25  10321  fin67  10392  axcclem  10454  canthp1lem2  10650  gchinf  10654  pwfseqlem4  10659  tskssel  10754  1nprm  16620  en2top  22708  domalom  36588  pibt2  36601  rp-isfinite6  42571  ensucne0OLD  42583  iscard5  42589  omiscard  42596
  Copyright terms: Public domain W3C validator