Theorem sdomnen 8930

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 497	1 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5100   ≈ 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-br 5101  df-sdom 8898

This theorem is referenced by:  bren2  8932  domdifsn  9000  sdomnsym  9042  domnsym  9043  sdomirr  9054  domnsymfi  9136  sucdom2  9139  php5  9147  phpeqd  9148  1sdom2dom  9166  pssinf  9174  f1finf1o  9185  isfinite2  9210  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  16618  en2top  22944  domalom  37663  pibt2  37676  rp-isfinite6  43878  ensucne0OLD  43890  iscard5  43896  omiscard  43903