Theorem sdomnen 8906

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5092   ≈ cen 8869   ≼ cdom 8870   ≺ csdm 8871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-br 5093  df-sdom 8875

This theorem is referenced by:  bren2  8908  domdifsn  8977  sdomnsym  9019  domnsym  9020  sdomirr  9031  domnsymfi  9114  sucdom2  9117  php5  9125  phpeqd  9126  1sdom2dom  9143  pssinf  9151  f1finf1o  9162  isfinite2  9187  cardom  9882  pm54.43  9897  alephdom  9975  cdainflem  10082  ackbij1b  10132  isfin4p1  10209  fin23lem25  10218  fin67  10289  axcclem  10351  canthp1lem2  10547  gchinf  10551  pwfseqlem4  10556  tskssel  10651  1nprm  16590  en2top  22870  domalom  37388  pibt2  37401  rp-isfinite6  43501  ensucne0OLD  43513  iscard5  43519  omiscard  43526