Theorem sdomdom 8928

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 8923	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
2	1	simplbi 497	1 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5102   ≈ cen 8892   ≼ cdom 8893   ≺ csdm 8894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-br 5103  df-sdom 8898

This theorem is referenced by:  domdifsn  9001  sdomnsym  9043  sdomdomtr  9051  domsdomtr  9053  sdomtr  9056  domnsymfi  9141  sdomdomtrfi  9142  domsdomtrfi  9143  sucdom2  9144  php3  9150  1sdom2dom  9170  sucxpdom  9178  findcard3  9205  isfinite2  9221  card2on  9483  fict  9582  fidomtri2  9923  prdom2  9935  infxpenlem  9942  indcardi  9970  alephnbtwn2  10001  alephsucdom  10008  alephdom  10010  dfac13  10072  djulepw  10122  infdjuabs  10134  infdif  10137  infunsdom1  10141  infunsdom  10142  infxp  10143  cfslb2n  10197  sdom2en01  10231  isfin32i  10294  fin34  10319  fin67  10324  hsmexlem1  10355  hsmex3  10363  entri3  10488  alephexp1  10508  gchdomtri  10558  canthp1  10583  pwfseqlem5  10592  gchdjuidm  10597  gchxpidm  10598  gchpwdom  10599  hargch  10602  gchaclem  10607  gchhar  10608  gchac  10610  inawinalem  10618  inar1  10704  rankcf  10706  tskuni  10712  grothac  10759  rpnnen  16171  rexpen  16172  aleph1irr  16190  dis1stc  23419  hauspwdom  23421  sibfof  34324  ctbssinf  37387  pibt2  37398  heiborlem3  37800  harinf  43016  saluncl  46308  meadjun  46453  meaiunlelem  46459  omeunle  46507