Theorem sdomnen 8974

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5109   ≈ cen 8936   ≼ cdom 8937   ≺ csdm 8938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-br 5110  df-sdom 8942

This theorem is referenced by:  bren2  8976  domdifsn  9044  sdomnsym  9086  domnsym  9087  sdomirr  9098  domnsymfi  9180  sucdom2  9183  php5  9191  phpeqd  9192  1sdom2dom  9210  pssinf  9218  f1finf1o  9229  isfinite2  9254  cardom  9968  pm54.43  9983  alephdom  10061  cdainflem  10167  ackbij1b  10217  isfin4p1  10294  fin23lem25  10303  fin67  10374  axcclem  10436  canthp1lem2  10633  gchinf  10637  pwfseqlem4  10642  tskssel  10737  1nprm  16732  en2top  23142  domalom  38070  pibt2  38083  rp-isfinite6  44264  ensucne0OLD  44276  iscard5  44282  omiscard  44289