Theorem sdomdom 8973

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5109   ≈ cen 8936   ≼ cdom 8937   ≺ csdm 8938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-br 5110  df-sdom 8942

This theorem is referenced by:  domdifsn  9044  sdomnsym  9086  sdomdomtr  9094  domsdomtr  9096  sdomtr  9099  domnsymfi  9180  sdomdomtrfi  9181  domsdomtrfi  9182  sucdom2  9183  php3  9189  1sdom2dom  9210  sucxpdom  9217  findcard3  9239  isfinite2  9254  card2on  9512  fict  9618  fidomtri2  9976  prdom2  9986  infxpenlem  9993  indcardi  10021  alephnbtwn2  10052  alephsucdom  10059  alephdom  10061  dfac13  10122  djulepw  10172  infdjuabs  10184  infdif  10187  infunsdom1  10191  infunsdom  10192  infxp  10193  cfslb2n  10247  sdom2en01  10281  isfin32i  10344  fin34  10369  fin67  10374  hsmexlem1  10405  hsmex3  10413  entri3  10538  alephexp1  10559  gchdomtri  10609  canthp1  10634  pwfseqlem5  10643  gchdjuidm  10648  gchxpidm  10649  gchpwdom  10650  hargch  10653  gchaclem  10658  gchhar  10659  gchac  10661  inawinalem  10669  inar1  10755  rankcf  10757  tskuni  10763  grothac  10810  rpnnen  16278  rexpen  16279  aleph1irr  16297  dis1stc  23656  hauspwdom  23658  sibfof  34730  ctbssinf  38072  pibt2  38083  heiborlem3  38484  harinf  43781  saluncl  47051  meadjun  47196  meaiunlelem  47202  omeunle  47250