Theorem sdomnen 8978

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5113   ≈ cen 8940   ≼ cdom 8941   ≺ csdm 8942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-br 5114  df-sdom 8946

This theorem is referenced by:  bren2  8980  domdifsn  9048  sdomnsym  9090  domnsym  9091  sdomirr  9102  domnsymfi  9184  sucdom2  9187  php5  9195  phpeqd  9196  1sdom2dom  9214  pssinf  9222  f1finf1o  9233  isfinite2  9258  cardom  9972  pm54.43  9987  alephdom  10065  cdainflem  10171  ackbij1b  10221  isfin4p1  10299  fin23lem25  10308  fin67  10379  axcclem  10441  canthp1lem2  10638  gchinf  10642  pwfseqlem4  10647  tskssel  10742  1nprm  16737  en2top  23111  domalom  37972  pibt2  37985  rp-isfinite6  44170  ensucne0OLD  44182  iscard5  44188  omiscard  44195