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

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

Proof of Theorem sdomdom
StepHypRef Expression
1 brsdom 8921 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
21simplbi 499 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   class class class wbr 5109  cen 8886  cdom 8887  csdm 8888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-dif 3917  df-br 5110  df-sdom 8892
This theorem is referenced by:  domdifsn  9004  sucdom2OLD  9032  sdomnsym  9048  sdomdomtr  9060  domsdomtr  9062  sdomtr  9065  domnsymfi  9153  sdomdomtrfi  9154  domsdomtrfi  9155  sucdom2  9156  php3  9162  1sdom2dom  9197  sucxpdom  9205  findcard3  9235  isfinite2  9251  pwfiOLD  9297  card2on  9498  fict  9597  fidomtri2  9938  prdom2  9950  infxpenlem  9957  indcardi  9985  alephnbtwn2  10016  alephsucdom  10023  alephdom  10025  dfac13  10086  djulepw  10136  infdjuabs  10150  infdif  10153  infunsdom1  10157  infunsdom  10158  infxp  10159  cfslb2n  10212  sdom2en01  10246  isfin32i  10309  fin34  10334  fin67  10339  hsmexlem1  10370  hsmex3  10378  entri3  10503  alephexp1  10523  gchdomtri  10573  canthp1  10598  pwfseqlem5  10607  gchdjuidm  10612  gchxpidm  10613  gchpwdom  10614  hargch  10617  gchaclem  10622  gchhar  10623  gchac  10625  inawinalem  10633  inar1  10719  rankcf  10721  tskuni  10727  grothac  10774  rpnnen  16117  rexpen  16118  aleph1irr  16136  dis1stc  22873  hauspwdom  22875  sibfof  33004  ctbssinf  35927  pibt2  35938  heiborlem3  36322  harinf  41405  saluncl  44648  meadjun  44793  meaiunlelem  44799  omeunle  44847
  Copyright terms: Public domain W3C validator