Theorem sdomdom 9040

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5166   ≈ cen 9000   ≼ cdom 9001   ≺ csdm 9002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-br 5167  df-sdom 9006

This theorem is referenced by:  domdifsn  9120  sucdom2OLD  9148  sdomnsym  9164  sdomdomtr  9176  domsdomtr  9178  sdomtr  9181  domnsymfi  9266  sdomdomtrfi  9267  domsdomtrfi  9268  sucdom2  9269  php3  9275  1sdom2dom  9310  sucxpdom  9318  findcard3  9346  isfinite2  9362  pwfiOLD  9417  card2on  9623  fict  9722  fidomtri2  10063  prdom2  10075  infxpenlem  10082  indcardi  10110  alephnbtwn2  10141  alephsucdom  10148  alephdom  10150  dfac13  10212  djulepw  10262  infdjuabs  10274  infdif  10277  infunsdom1  10281  infunsdom  10282  infxp  10283  cfslb2n  10337  sdom2en01  10371  isfin32i  10434  fin34  10459  fin67  10464  hsmexlem1  10495  hsmex3  10503  entri3  10628  alephexp1  10648  gchdomtri  10698  canthp1  10723  pwfseqlem5  10732  gchdjuidm  10737  gchxpidm  10738  gchpwdom  10739  hargch  10742  gchaclem  10747  gchhar  10748  gchac  10750  inawinalem  10758  inar1  10844  rankcf  10846  tskuni  10852  grothac  10899  rpnnen  16275  rexpen  16276  aleph1irr  16294  dis1stc  23528  hauspwdom  23530  sibfof  34305  ctbssinf  37372  pibt2  37383  heiborlem3  37773  harinf  42991  saluncl  46238  meadjun  46383  meaiunlelem  46389  omeunle  46437