Theorem sdomdom 8976

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5149   ≈ 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-br 5150  df-sdom 8942

This theorem is referenced by:  domdifsn  9054  sucdom2OLD  9082  sdomnsym  9098  sdomdomtr  9110  domsdomtr  9112  sdomtr  9115  domnsymfi  9203  sdomdomtrfi  9204  domsdomtrfi  9205  sucdom2  9206  php3  9212  1sdom2dom  9247  sucxpdom  9255  findcard3  9285  isfinite2  9301  pwfiOLD  9347  card2on  9549  fict  9648  fidomtri2  9989  prdom2  10001  infxpenlem  10008  indcardi  10036  alephnbtwn2  10067  alephsucdom  10074  alephdom  10076  dfac13  10137  djulepw  10187  infdjuabs  10201  infdif  10204  infunsdom1  10208  infunsdom  10209  infxp  10210  cfslb2n  10263  sdom2en01  10297  isfin32i  10360  fin34  10385  fin67  10390  hsmexlem1  10421  hsmex3  10429  entri3  10554  alephexp1  10574  gchdomtri  10624  canthp1  10649  pwfseqlem5  10658  gchdjuidm  10663  gchxpidm  10664  gchpwdom  10665  hargch  10668  gchaclem  10673  gchhar  10674  gchac  10676  inawinalem  10684  inar1  10770  rankcf  10772  tskuni  10778  grothac  10825  rpnnen  16170  rexpen  16171  aleph1irr  16189  dis1stc  23003  hauspwdom  23005  sibfof  33339  ctbssinf  36287  pibt2  36298  heiborlem3  36681  harinf  41773  saluncl  45033  meadjun  45178  meaiunlelem  45184  omeunle  45232