Theorem sdomdom 9018

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5105   ≈ cen 8981   ≼ cdom 8982   ≺ csdm 8983

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-dif 4049  df-br 5106  df-sdom 8987

This theorem is used by:  domdifsn  9090  sdomnsym  9132  sdomdomtr  9140  domsdomtr  9142  sdomtr  9145  domnsymfi  9226  sdomdomtrfi  9227  domsdomtrfi  9228  sucdom2  9229  php3  9235  1sdom2dom  9256  sucxpdom  9263  findcard3  9285  isfinite2  9301  card2on  9558  fict  9664  fidomtri2  10085  prdom2  10095  infxpenlem  10102  indcardi  10130  alephnbtwn2  10161  alephsucdom  10168  alephdom  10170  dfac13  10231  djulepw  10281  infdjuabs  10293  infdif  10296  infunsdom1  10300  infunsdom  10301  infxp  10302  cfslb2n  10356  sdom2en01  10390  isfin32i  10453  fin34  10478  fin67  10483  hsmexlem1  10514  hsmex3  10522  entri3  10653  alephexp1  10674  gchdomtri  10724  canthp1  10749  pwfseqlem5  10758  gchdjuidm  10763  gchxpidm  10764  gchpwdom  10765  hargch  10768  gchaclem  10773  gchhar  10774  gchac  10776  inawinalem  10784  inar1  10870  rankcf  10872  tskuni  10878  grothac  10925  rpnnen  16407  rexpen  16408  aleph1irr  16426  dis1stc  23830  hauspwdom  23832  sibfof  35025  dfac16  35825  ctbssinf  38469  heiborlem3  38887  harinf  44181  saluncl  47466  meadjun  47611  meaiunlelem  47617  omeunle  47665