Theorem sdomnen 8724

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5070   ≈ cen 8688   ≼ cdom 8689   ≺ csdm 8690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-br 5071  df-sdom 8694

This theorem is referenced by:  bren2  8726  domdifsn  8795  sucdom2  8822  sdomnsym  8838  domnsym  8839  sdomirr  8850  php5  8901  phpeqd  8902  pssinf  8962  f1finf1o  8975  isfinite2  9002  cardom  9675  pm54.43  9690  pr2ne  9692  alephdom  9768  cdainflem  9874  ackbij1b  9926  isfin4p1  10002  fin23lem25  10011  fin67  10082  axcclem  10144  canthp1lem2  10340  gchinf  10344  pwfseqlem4  10349  tskssel  10444  1nprm  16312  en2top  22043  domalom  35502  pibt2  35515  rp-isfinite6  41023  ensucne0OLD  41035  iscard5  41039