Theorem sdomnen 8977

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 498	1 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5149   ≈ cen 8936   ≼ cdom 8937   ≺ csdm 8938

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-br 5150  df-sdom 8942

This theorem is referenced by:  bren2  8979  domdifsn  9054  sucdom2OLD  9082  sdomnsym  9098  domnsym  9099  sdomirr  9114  domnsymfi  9203  sucdom2  9206  php5  9214  phpeqd  9215  phpeqdOLD  9225  1sdom2dom  9247  pssinf  9256  f1finf1o  9271  f1finf1oOLD  9272  isfinite2  9301  cardom  9981  pm54.43  9996  pr2neOLD  10000  alephdom  10076  cdainflem  10182  ackbij1b  10234  isfin4p1  10310  fin23lem25  10319  fin67  10390  axcclem  10452  canthp1lem2  10648  gchinf  10652  pwfseqlem4  10657  tskssel  10752  1nprm  16616  en2top  22488  domalom  36285  pibt2  36298  rp-isfinite6  42269  ensucne0OLD  42281  iscard5  42287  omiscard  42294