Theorem sdomdom 8531

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5058   ≈ cen 8500   ≼ cdom 8501   ≺ csdm 8502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938  df-br 5059  df-sdom 8506

This theorem is referenced by:  domdifsn  8594  sdomnsym  8636  sdomdomtr  8644  domsdomtr  8646  sdomtr  8649  sucdom2  8708  sucxpdom  8721  isfinite2  8770  pwfi  8813  card2on  9012  fict  9110  fidomtri2  9417  prdom2  9426  infxpenlem  9433  indcardi  9461  alephnbtwn2  9492  alephsucdom  9499  alephdom  9501  dfac13  9562  djulepw  9612  infdjuabs  9622  infdif  9625  infunsdom1  9629  infunsdom  9630  infxp  9631  cfslb2n  9684  sdom2en01  9718  isfin32i  9781  fin34  9806  fin67  9811  hsmexlem1  9842  hsmex3  9850  entri3  9975  alephexp1  9995  gchdomtri  10045  canthp1  10070  pwfseqlem5  10079  gchdjuidm  10084  gchxpidm  10085  gchpwdom  10086  hargch  10089  gchaclem  10094  gchhar  10095  gchac  10097  inawinalem  10105  inar1  10191  rankcf  10193  tskuni  10199  grothac  10246  rpnnen  15574  rexpen  15575  aleph1irr  15593  dis1stc  22101  hauspwdom  22103  sibfof  31593  ctbssinf  34681  pibt2  34692  heiborlem3  35085  harinf  39624  saluncl  42596  meadjun  42738  meaiunlelem  42744  omeunle  42792