Theorem sdomnen 9041

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5166   ≈ cen 9000   ≼ cdom 9001   ≺ csdm 9002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-br 5167  df-sdom 9006

This theorem is referenced by:  bren2  9043  domdifsn  9120  sucdom2OLD  9148  sdomnsym  9164  domnsym  9165  sdomirr  9180  domnsymfi  9266  sucdom2  9269  php5  9277  phpeqd  9278  phpeqdOLD  9288  1sdom2dom  9310  pssinf  9319  f1finf1o  9333  f1finf1oOLD  9334  isfinite2  9362  cardom  10055  pm54.43  10070  pr2neOLD  10074  alephdom  10150  cdainflem  10257  ackbij1b  10307  isfin4p1  10384  fin23lem25  10393  fin67  10464  axcclem  10526  canthp1lem2  10722  gchinf  10726  pwfseqlem4  10731  tskssel  10826  1nprm  16726  en2top  23013  domalom  37370  pibt2  37383  rp-isfinite6  43480  ensucne0OLD  43492  iscard5  43498  omiscard  43505