Theorem sdomnen 8928

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5085   ≈ cen 8890   ≼ cdom 8891   ≺ csdm 8892

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-br 5086  df-sdom 8896

This theorem is referenced by:  bren2  8930  domdifsn  8998  sdomnsym  9040  domnsym  9041  sdomirr  9052  domnsymfi  9134  sucdom2  9137  php5  9145  phpeqd  9146  1sdom2dom  9164  pssinf  9172  f1finf1o  9183  isfinite2  9208  cardom  9910  pm54.43  9925  alephdom  10003  cdainflem  10110  ackbij1b  10160  isfin4p1  10237  fin23lem25  10246  fin67  10317  axcclem  10379  canthp1lem2  10576  gchinf  10580  pwfseqlem4  10585  tskssel  10680  1nprm  16648  en2top  22950  domalom  37720  pibt2  37733  rp-isfinite6  43945  ensucne0OLD  43957  iscard5  43963  omiscard  43970