Theorem sdomdom 8520

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5030   ≈ cen 8489   ≼ cdom 8490   ≺ csdm 8491

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-br 5031  df-sdom 8495

This theorem is referenced by:  domdifsn  8583  sucdom2  8610  sdomnsym  8626  sdomdomtr  8634  domsdomtr  8636  sdomtr  8639  sucxpdom  8711  isfinite2  8760  pwfi  8803  card2on  9002  fict  9100  fidomtri2  9407  prdom2  9417  infxpenlem  9424  indcardi  9452  alephnbtwn2  9483  alephsucdom  9490  alephdom  9492  dfac13  9553  djulepw  9603  infdjuabs  9617  infdif  9620  infunsdom1  9624  infunsdom  9625  infxp  9626  cfslb2n  9679  sdom2en01  9713  isfin32i  9776  fin34  9801  fin67  9806  hsmexlem1  9837  hsmex3  9845  entri3  9970  alephexp1  9990  gchdomtri  10040  canthp1  10065  pwfseqlem5  10074  gchdjuidm  10079  gchxpidm  10080  gchpwdom  10081  hargch  10084  gchaclem  10089  gchhar  10090  gchac  10092  inawinalem  10100  inar1  10186  rankcf  10188  tskuni  10194  grothac  10241  rpnnen  15572  rexpen  15573  aleph1irr  15591  dis1stc  22104  hauspwdom  22106  sibfof  31708  ctbssinf  34823  pibt2  34834  heiborlem3  35251  harinf  39975  saluncl  42959  meadjun  43101  meaiunlelem  43107  omeunle  43155