Theorem sdomnen 5446

Description: Strict dominance implies non-equinumerosity.

Assertion

Ref	Expression
sdomnen	|- (A ~< B -> -. A ~~ B)

Proof of Theorem sdomnen

Step	Hyp	Ref	Expression
1		brsdom 5440	. 2 |- (A ~< B <-> (A ~<_ B /\ -. A ~~ B))
2	1	simprbi 353	1 |- (A ~< B -> -. A ~~ B)

Syntax hints:  -. wn 2   -> wi 3   class class class wbr 3338   ~~ cen 5423   ~<_ cdom 5424   ~< csdm 5425

This theorem is referenced by:  bren2 5448  sdomnsym 5525  domnsym 5526  sdomdomtr 5532  sdomirr 5535  php5 5611  pssinf 5621  isfinite2 5639  pm54.43 5662  cardnn 5870  cardom 5872  omsubsdom 5881  omsubdom 5882  omsubel 5883  ondomcard 6009  1nprm 13769  unpde2eg22 14407  top2ind 14897  tarsuc2 15245  carinttar 15279  omsubsdomOLD 15390  omsubdomOLD 15391  omsubelOLD 15392

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-dif 2597  df-br 3339  df-sdom 5429

Copyright terms: Public domain