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

Theorem sdomdom 6977
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 6972 . 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 4104    ~~ cen 6948    ~<_ cdom 6949    ~< csdm 6950
This theorem is referenced by:  domdifsn  7033  sdomnsym  7074  sdomdomtr  7082  domsdomtr  7084  sdomtr  7087  sucdom2  7145  sucxpdom  7160  isfinite2  7205  pwfi  7241  card2on  7358  fidomtri2  7717  prdom2  7726  infxpenlem  7731  indcardi  7758  alephnbtwn2  7789  alephsucdom  7796  alephdom  7798  dfac13  7858  cdalepw  7912  infcdaabs  7922  infdif  7925  infunsdom1  7929  infunsdom  7930  infxp  7931  cfslb2n  7984  sdom2en01  8018  isfin32i  8081  fin34  8106  fin67  8111  hsmexlem1  8142  hsmex3  8150  entri3  8271  unirnfdomd  8279  alephexp1  8291  cfpwsdom  8296  gchdomtri  8341  canthp1  8366  pwfseqlem5  8375  gchcdaidm  8380  gchxpidm  8381  gchaclem  8382  gchhar  8383  gchac  8385  gchpwdom  8386  hargch  8389  inawinalem  8401  inar1  8487  rankcf  8489  tskuni  8495  grothac  8542  rpnnen  12602  rexpen  12603  aleph1irr  12621  dis1stc  17331  hauspwdom  17333  ovolfi  18957  sigaclfu  23768  heiborlem3  25860  harinf  26450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-dif 3231  df-br 4105  df-sdom 6954
  Copyright terms: Public domain W3C validator