Theorem sdomnen 8769

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5074   ≈ cen 8730   ≼ cdom 8731   ≺ csdm 8732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-br 5075  df-sdom 8736

This theorem is referenced by:  bren2  8771  domdifsn  8841  sucdom2OLD  8869  sdomnsym  8885  domnsym  8886  sdomirr  8901  domnsymfi  8986  sucdom2  8989  php5  8997  phpeqd  8998  phpeqdOLD  9008  pssinf  9033  f1finf1o  9046  isfinite2  9072  cardom  9744  pm54.43  9759  pr2ne  9761  alephdom  9837  cdainflem  9943  ackbij1b  9995  isfin4p1  10071  fin23lem25  10080  fin67  10151  axcclem  10213  canthp1lem2  10409  gchinf  10413  pwfseqlem4  10418  tskssel  10513  1nprm  16384  en2top  22135  domalom  35575  pibt2  35588  rp-isfinite6  41125  ensucne0OLD  41137  iscard5  41143  omiscard  41150