Theorem sdomnen 9020

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5148   ≈ cen 8981   ≼ cdom 8982   ≺ csdm 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-br 5149  df-sdom 8987

This theorem is referenced by:  bren2  9022  domdifsn  9093  sucdom2OLD  9121  sdomnsym  9137  domnsym  9138  sdomirr  9153  domnsymfi  9238  sucdom2  9241  php5  9249  phpeqd  9250  phpeqdOLD  9260  1sdom2dom  9281  pssinf  9290  f1finf1o  9303  f1finf1oOLD  9304  isfinite2  9332  cardom  10024  pm54.43  10039  pr2neOLD  10043  alephdom  10119  cdainflem  10226  ackbij1b  10276  isfin4p1  10353  fin23lem25  10362  fin67  10433  axcclem  10495  canthp1lem2  10691  gchinf  10695  pwfseqlem4  10700  tskssel  10795  1nprm  16713  en2top  23008  domalom  37387  pibt2  37400  rp-isfinite6  43508  ensucne0OLD  43520  iscard5  43526  omiscard  43533