Theorem sdomdom 8842

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5093   ≈ cen 8802   ≼ cdom 8803   ≺ csdm 8804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-dif 3901  df-br 5094  df-sdom 8808

This theorem is referenced by:  domdifsn  8920  sucdom2OLD  8948  sdomnsym  8964  sdomdomtr  8976  domsdomtr  8978  sdomtr  8981  domnsymfi  9069  sdomdomtrfi  9070  domsdomtrfi  9071  sucdom2  9072  php3  9078  1sdom2dom  9113  sucxpdom  9121  findcard3  9151  isfinite2  9167  pwfiOLD  9213  card2on  9412  fict  9511  fidomtri2  9852  prdom2  9864  infxpenlem  9871  indcardi  9899  alephnbtwn2  9930  alephsucdom  9937  alephdom  9939  dfac13  10000  djulepw  10050  infdjuabs  10064  infdif  10067  infunsdom1  10071  infunsdom  10072  infxp  10073  cfslb2n  10126  sdom2en01  10160  isfin32i  10223  fin34  10248  fin67  10253  hsmexlem1  10284  hsmex3  10292  entri3  10417  alephexp1  10437  gchdomtri  10487  canthp1  10512  pwfseqlem5  10521  gchdjuidm  10526  gchxpidm  10527  gchpwdom  10528  hargch  10531  gchaclem  10536  gchhar  10537  gchac  10539  inawinalem  10547  inar1  10633  rankcf  10635  tskuni  10641  grothac  10688  rpnnen  16036  rexpen  16037  aleph1irr  16055  dis1stc  22757  hauspwdom  22759  sibfof  32607  ctbssinf  35733  pibt2  35744  heiborlem3  36127  harinf  41170  saluncl  44246  meadjun  44389  meaiunlelem  44395  omeunle  44443