Theorem sdomnen 8922

Description: Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)

Assertion

Ref	Expression
sdomnen	⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)

Proof of Theorem sdomnen

Step	Hyp	Ref	Expression
1		brsdom 8915	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
2	1	simprbi 497	1 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5086   ≈ cen 8884   ≼ cdom 8885   ≺ csdm 8886

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-br 5087  df-sdom 8890

This theorem is referenced by:  bren2  8924  domdifsn  8992  sdomnsym  9034  domnsym  9035  sdomirr  9046  domnsymfi  9128  sucdom2  9131  php5  9139  phpeqd  9140  1sdom2dom  9158  pssinf  9166  f1finf1o  9177  isfinite2  9202  cardom  9904  pm54.43  9919  alephdom  9997  cdainflem  10104  ackbij1b  10154  isfin4p1  10231  fin23lem25  10240  fin67  10311  axcclem  10373  canthp1lem2  10570  gchinf  10574  pwfseqlem4  10579  tskssel  10674  1nprm  16642  en2top  22963  domalom  37737  pibt2  37750  rp-isfinite6  43966  ensucne0OLD  43978  iscard5  43984  omiscard  43991