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

Theorem sdomdom 7098
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 7093 . 2  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
21simplbi 447 1  |-  ( A 
~<  B  ->  A  ~<_  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   class class class wbr 4176    ~~ cen 7069    ~<_ cdom 7070    ~< csdm 7071
This theorem is referenced by:  domdifsn  7154  sdomnsym  7195  sdomdomtr  7203  domsdomtr  7205  sdomtr  7208  sucdom2  7266  sucxpdom  7281  isfinite2  7328  pwfi  7364  card2on  7482  fidomtri2  7841  prdom2  7850  infxpenlem  7855  indcardi  7882  alephnbtwn2  7913  alephsucdom  7920  alephdom  7922  dfac13  7982  cdalepw  8036  infcdaabs  8046  infdif  8049  infunsdom1  8053  infunsdom  8054  infxp  8055  cfslb2n  8108  sdom2en01  8142  isfin32i  8205  fin34  8230  fin67  8235  hsmexlem1  8266  hsmex3  8274  entri3  8394  unirnfdomd  8402  alephexp1  8414  cfpwsdom  8419  gchdomtri  8464  canthp1  8489  pwfseqlem5  8498  gchcdaidm  8503  gchxpidm  8504  gchaclem  8505  gchhar  8506  gchac  8508  gchpwdom  8509  hargch  8512  inawinalem  8524  inar1  8610  rankcf  8612  tskuni  8618  grothac  8665  rpnnen  12785  rexpen  12786  aleph1irr  12804  dis1stc  17519  hauspwdom  17521  ovolfi  19347  sigaclfu  24459  sibfof  24611  heiborlem3  26416  harinf  26999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-dif 3287  df-br 4177  df-sdom 7075
  Copyright terms: Public domain W3C validator