Theorem sdomdom 9045

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5108   ≈ cen 9008   ≼ cdom 9009   ≺ csdm 9010

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-br 5109  df-sdom 9014

This theorem is used by:  domdifsn  9117  sdomnsym  9159  sdomdomtr  9167  domsdomtr  9169  sdomtr  9172  domnsymfi  9253  sdomdomtrfi  9254  domsdomtrfi  9255  sucdom2  9256  php3  9262  1sdom2dom  9283  sucxpdom  9290  findcard3  9312  isfinite2  9328  card2on  9585  fict  9691  fidomtri2  10114  prdom2  10124  infxpenlem  10131  indcardi  10159  alephnbtwn2  10190  alephsucdom  10197  alephdom  10199  dfac13  10260  djulepw  10310  infdjuabs  10322  infdif  10325  infunsdom1  10329  infunsdom  10330  infxp  10331  cfslb2n  10385  sdom2en01  10419  isfin32i  10482  fin34  10507  fin67  10512  hsmexlem1  10543  hsmex3  10551  entri3  10682  alephexp1  10703  gchdomtri  10753  canthp1  10778  pwfseqlem5  10787  gchdjuidm  10792  gchxpidm  10793  gchpwdom  10794  hargch  10797  gchaclem  10802  gchhar  10803  gchac  10805  inawinalem  10813  inar1  10899  rankcf  10901  tskuni  10907  grothac  10954  rpnnen  16439  rexpen  16440  aleph1irr  16458  dis1stc  23873  hauspwdom  23875  sibfof  35083  dfac16  35887  ctbssinf  38597  heiborlem3  39013  harinf  44307  saluncl  47600  meadjun  47745  meaiunlelem  47751  omeunle  47799