Theorem sdomdom 8902

Description: Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)

Assertion

Ref	Expression
sdomdom	⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)

Proof of Theorem sdomdom

Step	Hyp	Ref	Expression
1		brsdom 8897	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
2	1	simplbi 497	1 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5089   ≈ cen 8866   ≼ cdom 8867   ≺ csdm 8868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-br 5090  df-sdom 8872

This theorem is referenced by:  domdifsn  8973  sdomnsym  9015  sdomdomtr  9023  domsdomtr  9025  sdomtr  9028  domnsymfi  9109  sdomdomtrfi  9110  domsdomtrfi  9111  sucdom2  9112  php3  9118  1sdom2dom  9138  sucxpdom  9145  findcard3  9167  isfinite2  9182  card2on  9440  fict  9543  fidomtri2  9887  prdom2  9897  infxpenlem  9904  indcardi  9932  alephnbtwn2  9963  alephsucdom  9970  alephdom  9972  dfac13  10034  djulepw  10084  infdjuabs  10096  infdif  10099  infunsdom1  10103  infunsdom  10104  infxp  10105  cfslb2n  10159  sdom2en01  10193  isfin32i  10256  fin34  10281  fin67  10286  hsmexlem1  10317  hsmex3  10325  entri3  10450  alephexp1  10470  gchdomtri  10520  canthp1  10545  pwfseqlem5  10554  gchdjuidm  10559  gchxpidm  10560  gchpwdom  10561  hargch  10564  gchaclem  10569  gchhar  10570  gchac  10572  inawinalem  10580  inar1  10666  rankcf  10668  tskuni  10674  grothac  10721  rpnnen  16136  rexpen  16137  aleph1irr  16155  dis1stc  23414  hauspwdom  23416  sibfof  34353  ctbssinf  37450  pibt2  37461  heiborlem3  37863  harinf  43137  saluncl  46425  meadjun  46570  meaiunlelem  46576  omeunle  46624