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

Theorem sdomdom 7562
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 7557 . 2  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
21simplbi 460 1  |-  ( A 
~<  B  ->  A  ~<_  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   class class class wbr 4456    ~~ cen 7532    ~<_ cdom 7533    ~< csdm 7534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3474  df-br 4457  df-sdom 7538
This theorem is referenced by:  domdifsn  7619  sdomnsym  7661  sdomdomtr  7669  domsdomtr  7671  sdomtr  7674  sucdom2  7733  sucxpdom  7748  isfinite2  7796  pwfi  7833  card2on  7998  fidomtri2  8392  prdom2  8401  infxpenlem  8408  indcardi  8439  alephnbtwn2  8470  alephsucdom  8477  alephdom  8479  dfac13  8539  cdalepw  8593  infcdaabs  8603  infdif  8606  infunsdom1  8610  infunsdom  8611  infxp  8612  cfslb2n  8665  sdom2en01  8699  isfin32i  8762  fin34  8787  fin67  8792  hsmexlem1  8823  hsmex3  8831  entri3  8951  unirnfdomd  8959  alephexp1  8971  cfpwsdom  8976  gchdomtri  9024  canthp1  9049  pwfseqlem5  9058  gchcdaidm  9063  gchxpidm  9064  gchpwdom  9065  hargch  9068  gchaclem  9073  gchhar  9074  gchac  9076  inawinalem  9084  inar1  9170  rankcf  9172  tskuni  9178  grothac  9225  rpnnen  13972  rexpen  13973  aleph1irr  13991  dis1stc  20126  hauspwdom  20128  ovolfi  22031  fict  27687  sibfof  28479  heiborlem3  30514  harinf  31180
  Copyright terms: Public domain W3C validator