Theorem sdomnen 8919

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-br 5074  df-sdom 8887

This theorem is referenced by:  bren2  8921  domdifsn  8989  sdomnsym  9031  domnsym  9032  sdomirr  9043  domnsymfi  9125  sucdom2  9128  php5  9136  phpeqd  9137  1sdom2dom  9155  pssinf  9163  f1finf1o  9174  isfinite2  9199  cardom  9902  pm54.43  9917  alephdom  9995  cdainflem  10102  ackbij1b  10152  isfin4p1  10229  fin23lem25  10238  fin67  10309  axcclem  10371  canthp1lem2  10568  gchinf  10572  pwfseqlem4  10577  tskssel  10672  1nprm  16640  en2top  22969  domalom  37775  pibt2  37788  rp-isfinite6  43971  ensucne0OLD  43983  iscard5  43989  omiscard  43996