Theorem sdomdom 8983

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5111   ≈ cen 8946   ≼ cdom 8947   ≺ csdm 8948

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-br 5112  df-sdom 8952

This theorem is used by:  domdifsn  9055  sdomnsym  9097  sdomdomtr  9105  domsdomtr  9107  sdomtr  9110  domnsymfi  9191  sdomdomtrfi  9192  domsdomtrfi  9193  sucdom2  9194  php3  9200  1sdom2dom  9221  sucxpdom  9228  findcard3  9250  isfinite2  9265  card2on  9523  fict  9629  fidomtri2  9996  prdom2  10006  infxpenlem  10013  indcardi  10041  alephnbtwn2  10072  alephsucdom  10079  alephdom  10081  dfac13  10142  djulepw  10192  infdjuabs  10204  infdif  10207  infunsdom1  10211  infunsdom  10212  infxp  10213  cfslb2n  10267  sdom2en01  10301  isfin32i  10364  fin34  10389  fin67  10394  hsmexlem1  10425  hsmex3  10433  entri3  10560  alephexp1  10581  gchdomtri  10631  canthp1  10656  pwfseqlem5  10665  gchdjuidm  10670  gchxpidm  10671  gchpwdom  10672  hargch  10675  gchaclem  10680  gchhar  10681  gchac  10683  inawinalem  10691  inar1  10777  rankcf  10779  tskuni  10785  grothac  10832  rpnnen  16307  rexpen  16308  aleph1irr  16326  dis1stc  23709  hauspwdom  23711  sibfof  34797  ctbssinf  38111  pibt2  38122  heiborlem3  38524  harinf  43821  saluncl  47091  meadjun  47236  meaiunlelem  47242  omeunle  47290