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

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

Proof of Theorem sdomdom
StepHypRef Expression
1 brsdom 8530 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
21simplbi 501 1 (𝐴𝐵𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5053   ≈ cen 8504   ≼ cdom 8505   ≺ csdm 8506 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-dif 3922  df-br 5054  df-sdom 8510 This theorem is referenced by:  domdifsn  8598  sucdom2  8625  sdomnsym  8641  sdomdomtr  8649  domsdomtr  8651  sdomtr  8654  sucxpdom  8726  isfinite2  8775  pwfi  8818  card2on  9017  fict  9115  fidomtri2  9422  prdom2  9432  infxpenlem  9439  indcardi  9467  alephnbtwn2  9498  alephsucdom  9505  alephdom  9507  dfac13  9568  djulepw  9618  infdjuabs  9628  infdif  9631  infunsdom1  9635  infunsdom  9636  infxp  9637  cfslb2n  9690  sdom2en01  9724  isfin32i  9787  fin34  9812  fin67  9817  hsmexlem1  9848  hsmex3  9856  entri3  9981  alephexp1  10001  gchdomtri  10051  canthp1  10076  pwfseqlem5  10085  gchdjuidm  10090  gchxpidm  10091  gchpwdom  10092  hargch  10095  gchaclem  10100  gchhar  10101  gchac  10103  inawinalem  10111  inar1  10197  rankcf  10199  tskuni  10205  grothac  10252  rpnnen  15582  rexpen  15583  aleph1irr  15601  dis1stc  22113  hauspwdom  22115  sibfof  31683  ctbssinf  34795  pibt2  34806  heiborlem3  35223  harinf  39919  saluncl  42912  meadjun  43054  meaiunlelem  43060  omeunle  43108
 Copyright terms: Public domain W3C validator