Theorem sdomdom 9020

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5143   ≈ cen 8982   ≼ cdom 8983   ≺ csdm 8984

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-br 5144  df-sdom 8988

This theorem is referenced by:  domdifsn  9094  sucdom2OLD  9122  sdomnsym  9138  sdomdomtr  9150  domsdomtr  9152  sdomtr  9155  domnsymfi  9240  sdomdomtrfi  9241  domsdomtrfi  9242  sucdom2  9243  php3  9249  1sdom2dom  9283  sucxpdom  9291  findcard3  9318  isfinite2  9334  card2on  9594  fict  9693  fidomtri2  10034  prdom2  10046  infxpenlem  10053  indcardi  10081  alephnbtwn2  10112  alephsucdom  10119  alephdom  10121  dfac13  10183  djulepw  10233  infdjuabs  10245  infdif  10248  infunsdom1  10252  infunsdom  10253  infxp  10254  cfslb2n  10308  sdom2en01  10342  isfin32i  10405  fin34  10430  fin67  10435  hsmexlem1  10466  hsmex3  10474  entri3  10599  alephexp1  10619  gchdomtri  10669  canthp1  10694  pwfseqlem5  10703  gchdjuidm  10708  gchxpidm  10709  gchpwdom  10710  hargch  10713  gchaclem  10718  gchhar  10719  gchac  10721  inawinalem  10729  inar1  10815  rankcf  10817  tskuni  10823  grothac  10870  rpnnen  16263  rexpen  16264  aleph1irr  16282  dis1stc  23507  hauspwdom  23509  sibfof  34342  ctbssinf  37407  pibt2  37418  heiborlem3  37820  harinf  43046  saluncl  46332  meadjun  46477  meaiunlelem  46483  omeunle  46531