Theorem sdomdom 8188

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 4809   ≈ cen 8157   ≼ cdom 8158   ≺ csdm 8159

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-dif 3735  df-br 4810  df-sdom 8163

This theorem is referenced by:  domdifsn  8250  sdomnsym  8292  sdomdomtr  8300  domsdomtr  8302  sdomtr  8305  sucdom2  8363  sucxpdom  8376  isfinite2  8425  pwfi  8468  card2on  8666  fict  8765  fidomtri2  9071  prdom2  9080  infxpenlem  9087  indcardi  9115  alephnbtwn2  9146  alephsucdom  9153  alephdom  9155  dfac13  9217  cdalepw  9271  infcdaabs  9281  infdif  9284  infunsdom1  9288  infunsdom  9289  infxp  9290  cfslb2n  9343  sdom2en01  9377  isfin32i  9440  fin34  9465  fin67  9470  hsmexlem1  9501  hsmex3  9509  entri3  9634  unirnfdomd  9642  alephexp1  9654  cfpwsdom  9659  gchdomtri  9704  canthp1  9729  pwfseqlem5  9738  gchcdaidm  9743  gchxpidm  9744  gchpwdom  9745  hargch  9748  gchaclem  9753  gchhar  9754  gchac  9756  inawinalem  9764  inar1  9850  rankcf  9852  tskuni  9858  grothac  9905  rpnnen  15238  rexpen  15239  aleph1irr  15257  dis1stc  21582  hauspwdom  21584  ovolfi  23552  sibfof  30849  heiborlem3  34034  harinf  38278  saluncl  41174  meadjun  41316  meaiunlelem  41322  omeunle  41370