Theorem sdomnen 8920

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5098   ≈ cen 8882   ≼ cdom 8883   ≺ csdm 8884

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-br 5099  df-sdom 8888

This theorem is referenced by:  bren2  8922  domdifsn  8990  sdomnsym  9032  domnsym  9033  sdomirr  9044  domnsymfi  9126  sucdom2  9129  php5  9137  phpeqd  9138  1sdom2dom  9156  pssinf  9164  f1finf1o  9175  isfinite2  9200  cardom  9900  pm54.43  9915  alephdom  9993  cdainflem  10100  ackbij1b  10150  isfin4p1  10227  fin23lem25  10236  fin67  10307  axcclem  10369  canthp1lem2  10566  gchinf  10570  pwfseqlem4  10575  tskssel  10670  1nprm  16608  en2top  22931  domalom  37611  pibt2  37624  rp-isfinite6  43780  ensucne0OLD  43792  iscard5  43798  omiscard  43805