Theorem sdomnen 4528

Description: Strict dominance implies non-equinumerosity.

Assertion

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

Proof of Theorem sdomnen

Step	Hyp	Ref	Expression
1		brsdom 4522	. 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 2692   ~~ cen 4505   ~<_ cdom 4506   ~< csdm 4507

This theorem is referenced by:  bren2 4530  sdomnsym 4607  domnsym 4608  sdomdomtr 4614  sdomirr 4617  php5 4664  pssinf 4674  isfinite2 4692  pm54.43 4715  cardnn 4970  cardom 4972  ondomcard 5007  unpde2eg22 10826  top2ind 11050  omsubsdom 11442  omsubdom 11443  omsubel 11444

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-dif 2101  df-br 2693  df-sdom 4511

Copyright terms: Public domain