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

Theorem sdomdom 7535
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 7530 . 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 4442    ~~ cen 7505    ~<_ cdom 7506    ~< csdm 7507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-dif 3474  df-br 4443  df-sdom 7511
This theorem is referenced by:  domdifsn  7592  sdomnsym  7634  sdomdomtr  7642  domsdomtr  7644  sdomtr  7647  sucdom2  7706  sucxpdom  7721  isfinite2  7769  pwfi  7806  card2on  7971  fidomtri2  8366  prdom2  8375  infxpenlem  8382  indcardi  8413  alephnbtwn2  8444  alephsucdom  8451  alephdom  8453  dfac13  8513  cdalepw  8567  infcdaabs  8577  infdif  8580  infunsdom1  8584  infunsdom  8585  infxp  8586  cfslb2n  8639  sdom2en01  8673  isfin32i  8736  fin34  8761  fin67  8766  hsmexlem1  8797  hsmex3  8805  entri3  8925  unirnfdomd  8933  alephexp1  8945  cfpwsdom  8950  gchdomtri  8998  canthp1  9023  pwfseqlem5  9032  gchcdaidm  9037  gchxpidm  9038  gchpwdom  9039  hargch  9042  gchaclem  9047  gchhar  9048  gchac  9050  inawinalem  9058  inar1  9144  rankcf  9146  tskuni  9152  grothac  9199  rpnnen  13812  rexpen  13813  aleph1irr  13831  dis1stc  19761  hauspwdom  19763  ovolfi  21635  fict  27190  sigaclfu  27747  sibfof  27910  heiborlem3  29901  harinf  30571
  Copyright terms: Public domain W3C validator