Theorem sdomdom 8768

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5074   ≈ cen 8730   ≼ cdom 8731   ≺ csdm 8732

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-br 5075  df-sdom 8736

This theorem is referenced by:  domdifsn  8841  sucdom2OLD  8869  sdomnsym  8885  sdomdomtr  8897  domsdomtr  8899  sdomtr  8902  domnsymfi  8986  sdomdomtrfi  8987  domsdomtrfi  8988  sucdom2  8989  php3  8995  sucxpdom  9032  isfinite2  9072  pwfiOLD  9114  card2on  9313  fict  9411  fidomtri2  9752  prdom2  9762  infxpenlem  9769  indcardi  9797  alephnbtwn2  9828  alephsucdom  9835  alephdom  9837  dfac13  9898  djulepw  9948  infdjuabs  9962  infdif  9965  infunsdom1  9969  infunsdom  9970  infxp  9971  cfslb2n  10024  sdom2en01  10058  isfin32i  10121  fin34  10146  fin67  10151  hsmexlem1  10182  hsmex3  10190  entri3  10315  alephexp1  10335  gchdomtri  10385  canthp1  10410  pwfseqlem5  10419  gchdjuidm  10424  gchxpidm  10425  gchpwdom  10426  hargch  10429  gchaclem  10434  gchhar  10435  gchac  10437  inawinalem  10445  inar1  10531  rankcf  10533  tskuni  10539  grothac  10586  rpnnen  15936  rexpen  15937  aleph1irr  15955  dis1stc  22650  hauspwdom  22652  sibfof  32307  ctbssinf  35577  pibt2  35588  heiborlem3  35971  harinf  40856  saluncl  43858  meadjun  44000  meaiunlelem  44006  omeunle  44054