Theorem sdomnen 8929

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 8923	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
2	1	simprbi 496	1 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5102   ≈ cen 8892   ≼ cdom 8893   ≺ csdm 8894

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-br 5103  df-sdom 8898

This theorem is referenced by:  bren2  8931  domdifsn  9001  sdomnsym  9043  domnsym  9044  sdomirr  9055  domnsymfi  9141  sucdom2  9144  php5  9152  phpeqd  9153  1sdom2dom  9170  pssinf  9179  f1finf1o  9192  f1finf1oOLD  9193  isfinite2  9221  cardom  9915  pm54.43  9930  pr2neOLD  9934  alephdom  10010  cdainflem  10117  ackbij1b  10167  isfin4p1  10244  fin23lem25  10253  fin67  10324  axcclem  10386  canthp1lem2  10582  gchinf  10586  pwfseqlem4  10591  tskssel  10686  1nprm  16625  en2top  22905  domalom  37385  pibt2  37398  rp-isfinite6  43500  ensucne0OLD  43512  iscard5  43518  omiscard  43525