Theorem sdomnen 8977

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5113   ≈ cen 8939   ≼ cdom 8940   ≺ csdm 8941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-br 5114  df-sdom 8945

This theorem is referenced by:  bren2  8979  domdifsn  9047  sdomnsym  9089  domnsym  9090  sdomirr  9101  domnsymfi  9183  sucdom2  9186  php5  9194  phpeqd  9195  1sdom2dom  9213  pssinf  9221  f1finf1o  9232  isfinite2  9257  cardom  9971  pm54.43  9986  alephdom  10064  cdainflem  10170  ackbij1b  10220  isfin4p1  10298  fin23lem25  10307  fin67  10378  axcclem  10440  canthp1lem2  10637  gchinf  10641  pwfseqlem4  10646  tskssel  10741  1nprm  16736  en2top  23110  domalom  37937  pibt2  37950  rp-isfinite6  44135  ensucne0OLD  44147  iscard5  44153  omiscard  44160