Theorem sdomnen 8540

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5068   ≈ cen 8508   ≼ cdom 8509   ≺ csdm 8510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-br 5069  df-sdom 8514

This theorem is referenced by:  bren2  8542  domdifsn  8602  sdomnsym  8644  domnsym  8645  sdomirr  8656  php5  8707  phpeqd  8708  sucdom2  8716  pssinf  8730  f1finf1o  8747  isfinite2  8778  cardom  9417  pm54.43  9431  pr2ne  9433  alephdom  9509  cdainflem  9615  ackbij1b  9663  isfin4p1  9739  fin23lem25  9748  fin67  9819  axcclem  9881  canthp1lem2  10077  gchinf  10081  pwfseqlem4  10086  tskssel  10181  1nprm  16025  en2top  21595  domalom  34687  pibt2  34700  rp-isfinite6  39891  ensucne0OLD  39903  iscard5  39908