Theorem sdomdom 9000

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5143   ≈ cen 8960   ≼ cdom 8961   ≺ csdm 8962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3949  df-br 5144  df-sdom 8966

This theorem is referenced by:  domdifsn  9081  sucdom2OLD  9109  sdomnsym  9125  sdomdomtr  9137  domsdomtr  9139  sdomtr  9142  domnsymfi  9227  sdomdomtrfi  9228  domsdomtrfi  9229  sucdom2  9230  php3  9236  1sdom2dom  9271  sucxpdom  9279  findcard3  9309  isfinite2  9325  pwfiOLD  9381  card2on  9587  fict  9686  fidomtri2  10027  prdom2  10039  infxpenlem  10046  indcardi  10074  alephnbtwn2  10105  alephsucdom  10112  alephdom  10114  dfac13  10175  djulepw  10225  infdjuabs  10237  infdif  10240  infunsdom1  10244  infunsdom  10245  infxp  10246  cfslb2n  10299  sdom2en01  10333  isfin32i  10396  fin34  10421  fin67  10426  hsmexlem1  10457  hsmex3  10465  entri3  10590  alephexp1  10610  gchdomtri  10660  canthp1  10685  pwfseqlem5  10694  gchdjuidm  10699  gchxpidm  10700  gchpwdom  10701  hargch  10704  gchaclem  10709  gchhar  10710  gchac  10712  inawinalem  10720  inar1  10806  rankcf  10808  tskuni  10814  grothac  10861  rpnnen  16221  rexpen  16222  aleph1irr  16240  dis1stc  23488  hauspwdom  23490  sibfof  34184  ctbssinf  37123  pibt2  37134  heiborlem3  37524  harinf  42726  saluncl  45971  meadjun  46116  meaiunlelem  46122  omeunle  46170