Theorem sdomnen 8916

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5096   ≈ cen 8878   ≼ cdom 8879   ≺ csdm 8880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-br 5097  df-sdom 8884

This theorem is referenced by:  bren2  8918  domdifsn  8986  sdomnsym  9028  domnsym  9029  sdomirr  9040  domnsymfi  9122  sucdom2  9125  php5  9133  phpeqd  9134  1sdom2dom  9152  pssinf  9160  f1finf1o  9171  isfinite2  9196  cardom  9896  pm54.43  9911  alephdom  9989  cdainflem  10096  ackbij1b  10146  isfin4p1  10223  fin23lem25  10232  fin67  10303  axcclem  10365  canthp1lem2  10562  gchinf  10566  pwfseqlem4  10571  tskssel  10666  1nprm  16604  en2top  22927  domalom  37548  pibt2  37561  rp-isfinite6  43701  ensucne0OLD  43713  iscard5  43719  omiscard  43726