Theorem sdomdom 8929

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5100   ≈ cen 8892   ≼ cdom 8893   ≺ csdm 8894

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-br 5101  df-sdom 8898

This theorem is referenced by:  domdifsn  9000  sdomnsym  9042  sdomdomtr  9050  domsdomtr  9052  sdomtr  9055  domnsymfi  9136  sdomdomtrfi  9137  domsdomtrfi  9138  sucdom2  9139  php3  9145  1sdom2dom  9166  sucxpdom  9173  findcard3  9195  isfinite2  9210  card2on  9471  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  16164  rexpen  16165  aleph1irr  16183  dis1stc  23455  hauspwdom  23457  sibfof  34518  ctbssinf  37661  pibt2  37672  heiborlem3  38064  harinf  43391  saluncl  46675  meadjun  46820  meaiunlelem  46826  omeunle  46874