Theorem sdomnen 9019

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5105   ≈ cen 8981   ≼ cdom 8982   ≺ csdm 8983

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-dif 4049  df-br 5106  df-sdom 8987

This theorem is used by:  bren2  9021  domdifsn  9090  sdomnsym  9132  domnsym  9133  sdomirr  9144  domnsymfi  9226  sucdom2  9229  php5  9237  phpeqd  9238  1sdom2dom  9256  pssinf  9264  f1finf1o  9275  isfinite2  9301  cardom  10077  pm54.43  10092  alephdom  10170  cdainflem  10276  ackbij1b  10326  isfin4p1  10403  fin23lem25  10412  fin67  10483  axcclem  10545  canthp1lem2  10748  gchinf  10752  pwfseqlem4  10757  tskssel  10852  1nprm  16866  en2top  23315  domalom  38467  pibt2  38480  rp-isfinite6  44659  ensucne0OLD  44671  iscard5  44677  omiscard  44684