Theorem sdomdom 8905

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5092   ≈ cen 8869   ≼ cdom 8870   ≺ csdm 8871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-br 5093  df-sdom 8875

This theorem is referenced by:  domdifsn  8977  sdomnsym  9019  sdomdomtr  9027  domsdomtr  9029  sdomtr  9032  domnsymfi  9114  sdomdomtrfi  9115  domsdomtrfi  9116  sucdom2  9117  php3  9123  1sdom2dom  9143  sucxpdom  9150  findcard3  9172  isfinite2  9187  card2on  9446  fict  9549  fidomtri2  9890  prdom2  9900  infxpenlem  9907  indcardi  9935  alephnbtwn2  9966  alephsucdom  9973  alephdom  9975  dfac13  10037  djulepw  10087  infdjuabs  10099  infdif  10102  infunsdom1  10106  infunsdom  10107  infxp  10108  cfslb2n  10162  sdom2en01  10196  isfin32i  10259  fin34  10284  fin67  10289  hsmexlem1  10320  hsmex3  10328  entri3  10453  alephexp1  10473  gchdomtri  10523  canthp1  10548  pwfseqlem5  10557  gchdjuidm  10562  gchxpidm  10563  gchpwdom  10564  hargch  10567  gchaclem  10572  gchhar  10573  gchac  10575  inawinalem  10583  inar1  10669  rankcf  10671  tskuni  10677  grothac  10724  rpnnen  16136  rexpen  16137  aleph1irr  16155  dis1stc  23384  hauspwdom  23386  sibfof  34314  ctbssinf  37390  pibt2  37401  heiborlem3  37803  harinf  43017  saluncl  46308  meadjun  46453  meaiunlelem  46459  omeunle  46507