Theorem sdomdom 8921

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5086   ≈ cen 8884   ≼ cdom 8885   ≺ csdm 8886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-br 5087  df-sdom 8890

This theorem is referenced by:  domdifsn  8992  sdomnsym  9034  sdomdomtr  9042  domsdomtr  9044  sdomtr  9047  domnsymfi  9128  sdomdomtrfi  9129  domsdomtrfi  9130  sucdom2  9131  php3  9137  1sdom2dom  9158  sucxpdom  9165  findcard3  9187  isfinite2  9202  card2on  9463  fict  9568  fidomtri2  9912  prdom2  9922  infxpenlem  9929  indcardi  9957  alephnbtwn2  9988  alephsucdom  9995  alephdom  9997  dfac13  10059  djulepw  10109  infdjuabs  10121  infdif  10124  infunsdom1  10128  infunsdom  10129  infxp  10130  cfslb2n  10184  sdom2en01  10218  isfin32i  10281  fin34  10306  fin67  10311  hsmexlem1  10342  hsmex3  10350  entri3  10475  alephexp1  10496  gchdomtri  10546  canthp1  10571  pwfseqlem5  10580  gchdjuidm  10585  gchxpidm  10586  gchpwdom  10587  hargch  10590  gchaclem  10595  gchhar  10596  gchac  10598  inawinalem  10606  inar1  10692  rankcf  10694  tskuni  10700  grothac  10747  rpnnen  16188  rexpen  16189  aleph1irr  16207  dis1stc  23477  hauspwdom  23479  sibfof  34503  ctbssinf  37739  pibt2  37750  heiborlem3  38151  harinf  43483  saluncl  46766  meadjun  46911  meaiunlelem  46917  omeunle  46965