Theorem sdomdom 8537

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5066   ≈ cen 8506   ≼ cdom 8507   ≺ csdm 8508

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-br 5067  df-sdom 8512

This theorem is referenced by:  domdifsn  8600  sdomnsym  8642  sdomdomtr  8650  domsdomtr  8652  sdomtr  8655  sucdom2  8714  sucxpdom  8727  isfinite2  8776  pwfi  8819  card2on  9018  fict  9116  fidomtri2  9423  prdom2  9432  infxpenlem  9439  indcardi  9467  alephnbtwn2  9498  alephsucdom  9505  alephdom  9507  dfac13  9568  djulepw  9618  infdjuabs  9628  infdif  9631  infunsdom1  9635  infunsdom  9636  infxp  9637  cfslb2n  9690  sdom2en01  9724  isfin32i  9787  fin34  9812  fin67  9817  hsmexlem1  9848  hsmex3  9856  entri3  9981  alephexp1  10001  gchdomtri  10051  canthp1  10076  pwfseqlem5  10085  gchdjuidm  10090  gchxpidm  10091  gchpwdom  10092  hargch  10095  gchaclem  10100  gchhar  10101  gchac  10103  inawinalem  10111  inar1  10197  rankcf  10199  tskuni  10205  grothac  10252  rpnnen  15580  rexpen  15581  aleph1irr  15599  dis1stc  22107  hauspwdom  22109  sibfof  31598  ctbssinf  34690  pibt2  34701  heiborlem3  35106  harinf  39651  saluncl  42622  meadjun  42764  meaiunlelem  42770  omeunle  42818