Theorem sdomnen 8752

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5079   ≈ cen 8713   ≼ cdom 8714   ≺ csdm 8715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-dif 3895  df-br 5080  df-sdom 8719

This theorem is referenced by:  bren2  8754  domdifsn  8824  sucdom2  8851  sdomnsym  8867  domnsym  8868  sdomirr  8883  domnsymfi  8968  php5  8978  phpeqd  8979  phpeqdOLD  8990  pssinf  9011  f1finf1o  9024  isfinite2  9050  cardom  9745  pm54.43  9760  pr2ne  9762  alephdom  9838  cdainflem  9944  ackbij1b  9996  isfin4p1  10072  fin23lem25  10081  fin67  10152  axcclem  10214  canthp1lem2  10410  gchinf  10414  pwfseqlem4  10419  tskssel  10514  1nprm  16382  en2top  22133  domalom  35571  pibt2  35584  rp-isfinite6  41104  ensucne0OLD  41116  iscard5  41120