MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sdomdom Unicode version

Theorem sdomdom 6889
Description: Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
sdomdom  |-  ( A 
~<  B  ->  A  ~<_  B )

Proof of Theorem sdomdom
StepHypRef Expression
1 brsdom 6884 . 2  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
21simplbi 446 1  |-  ( A 
~<  B  ->  A  ~<_  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   class class class wbr 4023    ~~ cen 6860    ~<_ cdom 6861    ~< csdm 6862
This theorem is referenced by:  domdifsn  6945  sdomnsym  6986  sdomdomtr  6994  domsdomtr  6996  sdomtr  6999  sucdom2  7057  sucxpdom  7072  isfinite2  7115  pwfi  7151  card2on  7268  fidomtri2  7627  prdom2  7636  infxpenlem  7641  indcardi  7668  alephnbtwn2  7699  alephsucdom  7706  alephdom  7708  dfac13  7768  cdalepw  7822  infcdaabs  7832  infdif  7835  infunsdom1  7839  infunsdom  7840  infxp  7841  cfslb2n  7894  sdom2en01  7928  isfin32i  7991  fin34  8016  fin67  8021  hsmexlem1  8052  hsmex3  8060  entri3  8181  unirnfdomd  8189  alephexp1  8201  cfpwsdom  8206  gchdomtri  8251  canthp1  8276  pwfseqlem5  8285  gchcdaidm  8290  gchxpidm  8291  gchaclem  8292  gchhar  8293  gchac  8295  gchpwdom  8296  hargch  8299  inawinalem  8311  inar1  8397  rankcf  8399  tskuni  8405  grothac  8452  rpnnen  12505  rexpen  12506  aleph1irr  12524  dis1stc  17225  hauspwdom  17227  ovolfi  18853  sigaclfu  23480  heiborlem3  26537  harinf  27127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-br 4024  df-sdom 6866
  Copyright terms: Public domain W3C validator