Theorem sdomnen 8984

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5111   ≈ cen 8946   ≼ cdom 8947   ≺ csdm 8948

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-br 5112  df-sdom 8952

This theorem is used by:  bren2  8986  domdifsn  9055  sdomnsym  9097  domnsym  9098  sdomirr  9109  domnsymfi  9191  sucdom2  9194  php5  9202  phpeqd  9203  1sdom2dom  9221  pssinf  9229  f1finf1o  9240  isfinite2  9265  cardom  9988  pm54.43  10003  alephdom  10081  cdainflem  10187  ackbij1b  10237  isfin4p1  10314  fin23lem25  10323  fin67  10394  axcclem  10456  canthp1lem2  10655  gchinf  10659  pwfseqlem4  10664  tskssel  10759  1nprm  16761  en2top  23194  domalom  38109  pibt2  38122  rp-isfinite6  44304  ensucne0OLD  44316  iscard5  44322  omiscard  44329