Theorem sdomdom 8977

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5113   ≈ cen 8940   ≼ cdom 8941   ≺ csdm 8942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-br 5114  df-sdom 8946

This theorem is referenced by:  domdifsn  9048  sdomnsym  9090  sdomdomtr  9098  domsdomtr  9100  sdomtr  9103  domnsymfi  9184  sdomdomtrfi  9185  domsdomtrfi  9186  sucdom2  9187  php3  9193  1sdom2dom  9214  sucxpdom  9221  findcard3  9243  isfinite2  9258  card2on  9516  fict  9622  fidomtri2  9980  prdom2  9990  infxpenlem  9997  indcardi  10025  alephnbtwn2  10056  alephsucdom  10063  alephdom  10065  dfac13  10126  djulepw  10176  infdjuabs  10188  infdif  10191  infunsdom1  10195  infunsdom  10196  infxp  10197  cfslb2n  10252  sdom2en01  10286  isfin32i  10349  fin34  10374  fin67  10379  hsmexlem1  10410  hsmex3  10418  entri3  10543  alephexp1  10564  gchdomtri  10614  canthp1  10639  pwfseqlem5  10648  gchdjuidm  10653  gchxpidm  10654  gchpwdom  10655  hargch  10658  gchaclem  10663  gchhar  10664  gchac  10666  inawinalem  10674  inar1  10760  rankcf  10762  tskuni  10768  grothac  10815  rpnnen  16283  rexpen  16284  aleph1irr  16302  dis1stc  23625  hauspwdom  23627  sibfof  34675  ctbssinf  37940  pibt2  37951  heiborlem3  38352  harinf  43653  saluncl  46923  meadjun  47068  meaiunlelem  47074  omeunle  47122