Theorem sdomnen 9002

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5149   ≈ cen 8961   ≼ cdom 8962   ≺ csdm 8963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-br 5150  df-sdom 8967

This theorem is referenced by:  bren2  9004  domdifsn  9079  sucdom2OLD  9107  sdomnsym  9123  domnsym  9124  sdomirr  9139  domnsymfi  9228  sucdom2  9231  php5  9239  phpeqd  9240  phpeqdOLD  9250  1sdom2dom  9272  pssinf  9281  f1finf1o  9296  f1finf1oOLD  9297  isfinite2  9326  cardom  10011  pm54.43  10026  pr2neOLD  10030  alephdom  10106  cdainflem  10212  ackbij1b  10264  isfin4p1  10340  fin23lem25  10349  fin67  10420  axcclem  10482  canthp1lem2  10678  gchinf  10682  pwfseqlem4  10687  tskssel  10782  1nprm  16653  en2top  22932  domalom  37014  pibt2  37027  rp-isfinite6  43090  ensucne0OLD  43102  iscard5  43108  omiscard  43115