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

Theorem sdomdom 7551
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 7546 . 2  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
21simplbi 461 1  |-  ( A 
~<  B  ->  A  ~<_  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   class class class wbr 4366    ~~ cen 7521    ~<_ cdom 7522    ~< csdm 7523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-dif 3382  df-br 4367  df-sdom 7527
This theorem is referenced by:  domdifsn  7608  sdomnsym  7650  sdomdomtr  7658  domsdomtr  7660  sdomtr  7663  sucdom2  7721  sucxpdom  7734  isfinite2  7782  pwfi  7822  card2on  8022  fidomtri2  8380  prdom2  8389  infxpenlem  8396  indcardi  8423  alephnbtwn2  8454  alephsucdom  8461  alephdom  8463  dfac13  8523  cdalepw  8577  infcdaabs  8587  infdif  8590  infunsdom1  8594  infunsdom  8595  infxp  8596  cfslb2n  8649  sdom2en01  8683  isfin32i  8746  fin34  8771  fin67  8776  hsmexlem1  8807  hsmex3  8815  entri3  8935  unirnfdomd  8943  alephexp1  8955  cfpwsdom  8960  gchdomtri  9005  canthp1  9030  pwfseqlem5  9039  gchcdaidm  9044  gchxpidm  9045  gchpwdom  9046  hargch  9049  gchaclem  9054  gchhar  9055  gchac  9057  inawinalem  9065  inar1  9151  rankcf  9153  tskuni  9159  grothac  9206  rpnnen  14222  rexpen  14223  aleph1irr  14241  dis1stc  20456  hauspwdom  20458  ovolfi  22389  fict  28241  sibfof  29125  heiborlem3  32052  harinf  35802  saluncl  38042  meadjun  38151  meaiunlelem  38157  omeunle  38188
  Copyright terms: Public domain W3C validator