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

Theorem sdomdom 7437
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 7432 . 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 4390    ~~ cen 7407    ~<_ cdom 7408    ~< csdm 7409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-dif 3429  df-br 4391  df-sdom 7413
This theorem is referenced by:  domdifsn  7494  sdomnsym  7536  sdomdomtr  7544  domsdomtr  7546  sdomtr  7549  sucdom2  7608  sucxpdom  7623  isfinite2  7671  pwfi  7707  card2on  7870  fidomtri2  8265  prdom2  8274  infxpenlem  8281  indcardi  8312  alephnbtwn2  8343  alephsucdom  8350  alephdom  8352  dfac13  8412  cdalepw  8466  infcdaabs  8476  infdif  8479  infunsdom1  8483  infunsdom  8484  infxp  8485  cfslb2n  8538  sdom2en01  8572  isfin32i  8635  fin34  8660  fin67  8665  hsmexlem1  8696  hsmex3  8704  entri3  8824  unirnfdomd  8832  alephexp1  8844  cfpwsdom  8849  gchdomtri  8897  canthp1  8922  pwfseqlem5  8931  gchcdaidm  8936  gchxpidm  8937  gchpwdom  8938  hargch  8941  gchaclem  8946  gchhar  8947  gchac  8949  inawinalem  8957  inar1  9043  rankcf  9045  tskuni  9051  grothac  9098  rpnnen  13611  rexpen  13612  aleph1irr  13630  dis1stc  19219  hauspwdom  19221  ovolfi  21093  fict  26141  sigaclfu  26696  sibfof  26860  heiborlem3  28850  harinf  29521
  Copyright terms: Public domain W3C validator