Theorem sdomnen 7870

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 4583   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-br 4584  df-sdom 7844

This theorem is referenced by:  bren2  7872  domdifsn  7928  sdomnsym  7970  domnsym  7971  sdomirr  7982  php5  8033  sucdom2  8041  pssinf  8055  f1finf1o  8072  isfinite2  8103  cardom  8695  pm54.43  8709  pr2ne  8711  alephdom  8787  cdainflem  8896  ackbij1b  8944  isfin4-3  9020  fin23lem25  9029  fin67  9100  axcclem  9162  canthp1lem2  9354  gchinf  9358  pwfseqlem4  9363  tskssel  9458  1nprm  15230  en2top  20600  rp-isfinite6  36883