Theorem sdomnen 8386

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 4962   ≈ cen 8354   ≼ cdom 8355   ≺ csdm 8356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-dif 3862  df-br 4963  df-sdom 8360

This theorem is referenced by:  bren2  8388  domdifsn  8447  sdomnsym  8489  domnsym  8490  sdomirr  8501  php5  8552  sucdom2  8560  pssinf  8574  f1finf1o  8591  isfinite2  8622  cardom  9261  pm54.43  9275  pr2ne  9277  alephdom  9353  cdainflem  9459  ackbij1b  9507  isfin4p1  9583  fin23lem25  9592  fin67  9663  axcclem  9725  canthp1lem2  9921  gchinf  9925  pwfseqlem4  9930  tskssel  10025  1nprm  15852  en2top  21277  domalom  34216  pibt2  34229  rp-isfinite6  39369  ensucne0OLD  39381  iscard5  39386  rr-php2d  40053