Theorem sdomnen 8990

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5103   ≈ cen 8952   ≼ cdom 8953   ≺ csdm 8954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-br 5104  df-sdom 8958

This theorem is used by:  bren2  8992  domdifsn  9061  sdomnsym  9103  domnsym  9104  sdomirr  9115  domnsymfi  9197  sucdom2  9200  php5  9208  phpeqd  9209  1sdom2dom  9227  pssinf  9235  f1finf1o  9246  isfinite2  9271  cardom  9994  pm54.43  10009  alephdom  10087  cdainflem  10193  ackbij1b  10243  isfin4p1  10320  fin23lem25  10329  fin67  10400  axcclem  10462  canthp1lem2  10665  gchinf  10669  pwfseqlem4  10674  tskssel  10769  1nprm  16772  en2top  23213  domalom  38161  pibt2  38174  rp-isfinite6  44361  ensucne0OLD  44373  iscard5  44379  omiscard  44386