Theorem sdomnen 8952

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5107   ≈ cen 8915   ≼ cdom 8916   ≺ csdm 8917

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 3449  df-dif 3917  df-br 5108  df-sdom 8921

This theorem is referenced by:  bren2  8954  domdifsn  9024  sdomnsym  9066  domnsym  9067  sdomirr  9078  domnsymfi  9164  sucdom2  9167  php5  9175  phpeqd  9176  1sdom2dom  9194  pssinf  9203  f1finf1o  9216  f1finf1oOLD  9217  isfinite2  9245  cardom  9939  pm54.43  9954  pr2neOLD  9958  alephdom  10034  cdainflem  10141  ackbij1b  10191  isfin4p1  10268  fin23lem25  10277  fin67  10348  axcclem  10410  canthp1lem2  10606  gchinf  10610  pwfseqlem4  10615  tskssel  10710  1nprm  16649  en2top  22872  domalom  37392  pibt2  37405  rp-isfinite6  43507  ensucne0OLD  43519  iscard5  43525  omiscard  43532