Theorem sdomdom 8927

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5085   ≈ cen 8890   ≼ cdom 8891   ≺ csdm 8892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-br 5086  df-sdom 8896

This theorem is referenced by:  domdifsn  8998  sdomnsym  9040  sdomdomtr  9048  domsdomtr  9050  sdomtr  9053  domnsymfi  9134  sdomdomtrfi  9135  domsdomtrfi  9136  sucdom2  9137  php3  9143  1sdom2dom  9164  sucxpdom  9171  findcard3  9193  isfinite2  9208  card2on  9469  fict  9574  fidomtri2  9918  prdom2  9928  infxpenlem  9935  indcardi  9963  alephnbtwn2  9994  alephsucdom  10001  alephdom  10003  dfac13  10065  djulepw  10115  infdjuabs  10127  infdif  10130  infunsdom1  10134  infunsdom  10135  infxp  10136  cfslb2n  10190  sdom2en01  10224  isfin32i  10287  fin34  10312  fin67  10317  hsmexlem1  10348  hsmex3  10356  entri3  10481  alephexp1  10502  gchdomtri  10552  canthp1  10577  pwfseqlem5  10586  gchdjuidm  10591  gchxpidm  10592  gchpwdom  10593  hargch  10596  gchaclem  10601  gchhar  10602  gchac  10604  inawinalem  10612  inar1  10698  rankcf  10700  tskuni  10706  grothac  10753  rpnnen  16194  rexpen  16195  aleph1irr  16213  dis1stc  23464  hauspwdom  23466  sibfof  34484  ctbssinf  37722  pibt2  37733  heiborlem3  38134  harinf  43462  saluncl  46745  meadjun  46890  meaiunlelem  46896  omeunle  46944