Theorem sdomnen 9022

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5142   ≈ cen 8983   ≼ cdom 8984   ≺ csdm 8985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-dif 3953  df-br 5143  df-sdom 8989

This theorem is referenced by:  bren2  9024  domdifsn  9095  sucdom2OLD  9123  sdomnsym  9139  domnsym  9140  sdomirr  9155  domnsymfi  9241  sucdom2  9244  php5  9252  phpeqd  9253  phpeqdOLD  9263  1sdom2dom  9284  pssinf  9293  f1finf1o  9306  f1finf1oOLD  9307  isfinite2  9335  cardom  10027  pm54.43  10042  pr2neOLD  10046  alephdom  10122  cdainflem  10229  ackbij1b  10279  isfin4p1  10356  fin23lem25  10365  fin67  10436  axcclem  10498  canthp1lem2  10694  gchinf  10698  pwfseqlem4  10703  tskssel  10798  1nprm  16717  en2top  22993  domalom  37406  pibt2  37419  rp-isfinite6  43536  ensucne0OLD  43548  iscard5  43554  omiscard  43561