Theorem sdomdom 8961

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5100   ≈ cen 8924   ≼ cdom 8925   ≺ csdm 8926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-br 5101  df-sdom 8930

This theorem is referenced by:  domdifsn  9032  sdomnsym  9074  sdomdomtr  9082  domsdomtr  9084  sdomtr  9087  domnsymfi  9168  sdomdomtrfi  9169  domsdomtrfi  9170  sucdom2  9171  php3  9177  1sdom2dom  9198  sucxpdom  9205  findcard3  9227  isfinite2  9242  card2on  9502  fict  9608  fidomtri2  9952  prdom2  9962  infxpenlem  9969  indcardi  9997  alephnbtwn2  10028  alephsucdom  10035  alephdom  10037  dfac13  10099  djulepw  10149  infdjuabs  10161  infdif  10164  infunsdom1  10168  infunsdom  10169  infxp  10170  cfslb2n  10225  sdom2en01  10259  isfin32i  10322  fin34  10347  fin67  10352  hsmexlem1  10383  hsmex3  10391  entri3  10516  alephexp1  10537  gchdomtri  10587  canthp1  10612  pwfseqlem5  10621  gchdjuidm  10626  gchxpidm  10627  gchpwdom  10628  hargch  10631  gchaclem  10636  gchhar  10637  gchac  10639  inawinalem  10647  inar1  10733  rankcf  10735  tskuni  10741  grothac  10788  rpnnen  16259  rexpen  16260  aleph1irr  16278  dis1stc  23559  hauspwdom  23561  sibfof  34637  ctbssinf  37900  pibt2  37911  heiborlem3  38312  harinf  43611  saluncl  46891  meadjun  47036  meaiunlelem  47042  omeunle  47090