Theorem sdomnen 8635

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5039   ≈ cen 8601   ≼ cdom 8602   ≺ csdm 8603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-br 5040  df-sdom 8607

This theorem is referenced by:  bren2  8637  domdifsn  8706  sucdom2  8733  sdomnsym  8749  domnsym  8750  sdomirr  8761  php5  8812  phpeqd  8813  pssinf  8864  f1finf1o  8880  isfinite2  8907  cardom  9567  pm54.43  9582  pr2ne  9584  alephdom  9660  cdainflem  9766  ackbij1b  9818  isfin4p1  9894  fin23lem25  9903  fin67  9974  axcclem  10036  canthp1lem2  10232  gchinf  10236  pwfseqlem4  10241  tskssel  10336  1nprm  16199  en2top  21836  domalom  35261  pibt2  35274  rp-isfinite6  40751  ensucne0OLD  40763  iscard5  40767