Theorem sdomdom 8917

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5098   ≈ cen 8880   ≼ cdom 8881   ≺ csdm 8882

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-br 5099  df-sdom 8886

This theorem is referenced by:  domdifsn  8988  sdomnsym  9030  sdomdomtr  9038  domsdomtr  9040  sdomtr  9043  domnsymfi  9124  sdomdomtrfi  9125  domsdomtrfi  9126  sucdom2  9127  php3  9133  1sdom2dom  9154  sucxpdom  9161  findcard3  9183  isfinite2  9198  card2on  9459  fict  9562  fidomtri2  9906  prdom2  9916  infxpenlem  9923  indcardi  9951  alephnbtwn2  9982  alephsucdom  9989  alephdom  9991  dfac13  10053  djulepw  10103  infdjuabs  10115  infdif  10118  infunsdom1  10122  infunsdom  10123  infxp  10124  cfslb2n  10178  sdom2en01  10212  isfin32i  10275  fin34  10300  fin67  10305  hsmexlem1  10336  hsmex3  10344  entri3  10469  alephexp1  10490  gchdomtri  10540  canthp1  10565  pwfseqlem5  10574  gchdjuidm  10579  gchxpidm  10580  gchpwdom  10581  hargch  10584  gchaclem  10589  gchhar  10590  gchac  10592  inawinalem  10600  inar1  10686  rankcf  10688  tskuni  10694  grothac  10741  rpnnen  16152  rexpen  16153  aleph1irr  16171  dis1stc  23443  hauspwdom  23445  sibfof  34497  ctbssinf  37611  pibt2  37622  heiborlem3  38014  harinf  43286  saluncl  46571  meadjun  46716  meaiunlelem  46722  omeunle  46770