Theorem sdomnen 8963

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5101   ≈ cen 8925   ≼ cdom 8926   ≺ csdm 8927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-br 5102  df-sdom 8931

This theorem is referenced by:  bren2  8965  domdifsn  9033  sdomnsym  9075  domnsym  9076  sdomirr  9087  domnsymfi  9169  sucdom2  9172  php5  9180  phpeqd  9181  1sdom2dom  9199  pssinf  9207  f1finf1o  9218  isfinite2  9243  cardom  9945  pm54.43  9960  alephdom  10038  cdainflem  10145  ackbij1b  10195  isfin4p1  10273  fin23lem25  10282  fin67  10353  axcclem  10415  canthp1lem2  10612  gchinf  10616  pwfseqlem4  10621  tskssel  10716  1nprm  16714  en2top  23046  domalom  37899  pibt2  37912  rp-isfinite6  44095  ensucne0OLD  44107  iscard5  44113  omiscard  44120