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

Theorem sdomdom 7563
Description: Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)
Assertion
Ref Expression
sdomdom

Proof of Theorem sdomdom
StepHypRef Expression
1 brsdom 7558 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4   class class class wbr 4452   cen 7533   cdom 7534   csdm 7535
This theorem is referenced by:  domdifsn  7620  sdomnsym  7662  sdomdomtr  7670  domsdomtr  7672  sdomtr  7675  sucdom2  7734  sucxpdom  7749  isfinite2  7798  pwfi  7835  card2on  8001  fidomtri2  8396  prdom2  8405  infxpenlem  8412  indcardi  8443  alephnbtwn2  8474  alephsucdom  8481  alephdom  8483  dfac13  8543  cdalepw  8597  infcdaabs  8607  infdif  8610  infunsdom1  8614  infunsdom  8615  infxp  8616  cfslb2n  8669  sdom2en01  8703  isfin32i  8766  fin34  8791  fin67  8796  hsmexlem1  8827  hsmex3  8835  entri3  8955  unirnfdomd  8963  alephexp1  8975  cfpwsdom  8980  gchdomtri  9028  canthp1  9053  pwfseqlem5  9062  gchcdaidm  9067  gchxpidm  9068  gchpwdom  9069  hargch  9072  gchaclem  9077  gchhar  9078  gchac  9080  inawinalem  9088  inar1  9174  rankcf  9176  tskuni  9182  grothac  9229  rpnnen  13960  rexpen  13961  aleph1irr  13979  dis1stc  20000  hauspwdom  20002  ovolfi  21905  fict  27530  sibfof  28282  heiborlem3  30309  harinf  30976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-br 4453  df-sdom 7539
  Copyright terms: Public domain W3C validator