Theorem sdomnen 9000

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5124   ≈ cen 8961   ≼ cdom 8962   ≺ csdm 8963

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-br 5125  df-sdom 8967

This theorem is referenced by:  bren2  9002  domdifsn  9073  sucdom2OLD  9101  sdomnsym  9117  domnsym  9118  sdomirr  9133  domnsymfi  9219  sucdom2  9222  php5  9230  phpeqd  9231  phpeqdOLD  9239  1sdom2dom  9260  pssinf  9269  f1finf1o  9282  f1finf1oOLD  9283  isfinite2  9311  cardom  10005  pm54.43  10020  pr2neOLD  10024  alephdom  10100  cdainflem  10207  ackbij1b  10257  isfin4p1  10334  fin23lem25  10343  fin67  10414  axcclem  10476  canthp1lem2  10672  gchinf  10676  pwfseqlem4  10681  tskssel  10776  1nprm  16703  en2top  22928  domalom  37427  pibt2  37440  rp-isfinite6  43509  ensucne0OLD  43521  iscard5  43527  omiscard  43534