Theorem sdomnen 9008

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5103   ≈ cen 8970   ≼ cdom 8971   ≺ csdm 8972

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-br 5104  df-sdom 8976

This theorem is used by:  bren2  9010  domdifsn  9079  sdomnsym  9121  domnsym  9122  sdomirr  9133  domnsymfi  9215  sucdom2  9218  php5  9226  phpeqd  9227  1sdom2dom  9245  pssinf  9253  f1finf1o  9264  isfinite2  9290  cardom  10067  pm54.43  10082  alephdom  10160  cdainflem  10266  ackbij1b  10316  isfin4p1  10393  fin23lem25  10402  fin67  10473  axcclem  10535  canthp1lem2  10738  gchinf  10742  pwfseqlem4  10747  tskssel  10842  1nprm  16854  en2top  23303  domalom  38327  pibt2  38340  rp-isfinite6  44518  ensucne0OLD  44530  iscard5  44536  omiscard  44543