Theorem sdomnen 7984

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 4653   ≈ cen 7952   ≼ cdom 7953   ≺ csdm 7954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-br 4654  df-sdom 7958

This theorem is referenced by:  bren2  7986  domdifsn  8043  sdomnsym  8085  domnsym  8086  sdomirr  8097  php5  8148  sucdom2  8156  pssinf  8170  f1finf1o  8187  isfinite2  8218  cardom  8812  pm54.43  8826  pr2ne  8828  alephdom  8904  cdainflem  9013  ackbij1b  9061  isfin4-3  9137  fin23lem25  9146  fin67  9217  axcclem  9279  canthp1lem2  9475  gchinf  9479  pwfseqlem4  9484  tskssel  9579  1nprm  15392  en2top  20789  rp-isfinite6  37864