Theorem sdomdom 8915

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5096   ≈ cen 8878   ≼ cdom 8879   ≺ csdm 8880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-br 5097  df-sdom 8884

This theorem is referenced by:  domdifsn  8986  sdomnsym  9028  sdomdomtr  9036  domsdomtr  9038  sdomtr  9041  domnsymfi  9122  sdomdomtrfi  9123  domsdomtrfi  9124  sucdom2  9125  php3  9131  1sdom2dom  9152  sucxpdom  9159  findcard3  9181  isfinite2  9196  card2on  9457  fict  9560  fidomtri2  9904  prdom2  9914  infxpenlem  9921  indcardi  9949  alephnbtwn2  9980  alephsucdom  9987  alephdom  9989  dfac13  10051  djulepw  10101  infdjuabs  10113  infdif  10116  infunsdom1  10120  infunsdom  10121  infxp  10122  cfslb2n  10176  sdom2en01  10210  isfin32i  10273  fin34  10298  fin67  10303  hsmexlem1  10334  hsmex3  10342  entri3  10467  alephexp1  10488  gchdomtri  10538  canthp1  10563  pwfseqlem5  10572  gchdjuidm  10577  gchxpidm  10578  gchpwdom  10579  hargch  10582  gchaclem  10587  gchhar  10588  gchac  10590  inawinalem  10598  inar1  10684  rankcf  10686  tskuni  10692  grothac  10739  rpnnen  16150  rexpen  16151  aleph1irr  16169  dis1stc  23441  hauspwdom  23443  sibfof  34446  ctbssinf  37550  pibt2  37561  heiborlem3  37953  harinf  43218  saluncl  46503  meadjun  46648  meaiunlelem  46654  omeunle  46702