Theorem sdomdom 8999

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5124   ≈ cen 8961   ≼ cdom 8962   ≺ csdm 8963

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-br 5125  df-sdom 8967

This theorem is referenced by:  domdifsn  9073  sucdom2OLD  9101  sdomnsym  9117  sdomdomtr  9129  domsdomtr  9131  sdomtr  9134  domnsymfi  9219  sdomdomtrfi  9220  domsdomtrfi  9221  sucdom2  9222  php3  9228  1sdom2dom  9260  sucxpdom  9268  findcard3  9295  isfinite2  9311  card2on  9573  fict  9672  fidomtri2  10013  prdom2  10025  infxpenlem  10032  indcardi  10060  alephnbtwn2  10091  alephsucdom  10098  alephdom  10100  dfac13  10162  djulepw  10212  infdjuabs  10224  infdif  10227  infunsdom1  10231  infunsdom  10232  infxp  10233  cfslb2n  10287  sdom2en01  10321  isfin32i  10384  fin34  10409  fin67  10414  hsmexlem1  10445  hsmex3  10453  entri3  10578  alephexp1  10598  gchdomtri  10648  canthp1  10673  pwfseqlem5  10682  gchdjuidm  10687  gchxpidm  10688  gchpwdom  10689  hargch  10692  gchaclem  10697  gchhar  10698  gchac  10700  inawinalem  10708  inar1  10794  rankcf  10796  tskuni  10802  grothac  10849  rpnnen  16250  rexpen  16251  aleph1irr  16269  dis1stc  23442  hauspwdom  23444  sibfof  34377  ctbssinf  37429  pibt2  37440  heiborlem3  37842  harinf  43025  saluncl  46313  meadjun  46458  meaiunlelem  46464  omeunle  46512