Theorem sdomdom 8951

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5107   ≈ cen 8915   ≼ cdom 8916   ≺ csdm 8917

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 3449  df-dif 3917  df-br 5108  df-sdom 8921

This theorem is referenced by:  domdifsn  9024  sdomnsym  9066  sdomdomtr  9074  domsdomtr  9076  sdomtr  9079  domnsymfi  9164  sdomdomtrfi  9165  domsdomtrfi  9166  sucdom2  9167  php3  9173  1sdom2dom  9194  sucxpdom  9202  findcard3  9229  isfinite2  9245  card2on  9507  fict  9606  fidomtri2  9947  prdom2  9959  infxpenlem  9966  indcardi  9994  alephnbtwn2  10025  alephsucdom  10032  alephdom  10034  dfac13  10096  djulepw  10146  infdjuabs  10158  infdif  10161  infunsdom1  10165  infunsdom  10166  infxp  10167  cfslb2n  10221  sdom2en01  10255  isfin32i  10318  fin34  10343  fin67  10348  hsmexlem1  10379  hsmex3  10387  entri3  10512  alephexp1  10532  gchdomtri  10582  canthp1  10607  pwfseqlem5  10616  gchdjuidm  10621  gchxpidm  10622  gchpwdom  10623  hargch  10626  gchaclem  10631  gchhar  10632  gchac  10634  inawinalem  10642  inar1  10728  rankcf  10730  tskuni  10736  grothac  10783  rpnnen  16195  rexpen  16196  aleph1irr  16214  dis1stc  23386  hauspwdom  23388  sibfof  34331  ctbssinf  37394  pibt2  37405  heiborlem3  37807  harinf  43023  saluncl  46315  meadjun  46460  meaiunlelem  46466  omeunle  46514