Theorem sdomnen 4526

Description: Strict dominance implies non-equinumerosity.

Assertion

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

Proof of Theorem sdomnen

Step	Hyp	Ref	Expression
1		brsdom 4520	. 2 |- (A ~< B <-> (A ~<_ B /\ -. A ~~ B))
2	1	pm3.27bi 324	1 |- (A ~< B -> -. A ~~ B)

Syntax hints:  -. wn 2   -> wi 3   class class class wbr 2691   ~~ cen 4503   ~<_ cdom 4504   ~< csdm 4505

This theorem is referenced by:  bren2 4528  sdomnsym 4605  domnsym 4606  sdomdomtr 4612  sdomirr 4615  php5 4662  pssinf 4672  isfinite2 4690  pm54.43 4713  cardnn 4968  cardom 4970  ondomcard 5005  top2ind 11014  omsubsdom 11402  omsubdom 11403  omsubel 11404

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 997  ax-gen 998  ax-8 999  ax-10 1001  ax-12 1003  ax-17 1006  ax-4 1008  ax-5o 1010  ax-6o 1013  ax-9o 1158  ax-10o 1176  ax-16 1246  ax-11o 1254  ax-ext 1499

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1016  df-sb 1208  df-clab 1505  df-cleq 1510  df-clel 1513  df-v 1857  df-dif 2100  df-br 2692  df-sdom 4509

Copyright terms: Public domain