Theorem sdomdom 8917

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5072   ≈ cen 8880   ≼ cdom 8881   ≺ csdm 8882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-br 5073  df-sdom 8886

This theorem is referenced by:  domdifsn  8988  sdomnsym  9030  sdomdomtr  9038  domsdomtr  9040  sdomtr  9043  domnsymfi  9124  sdomdomtrfi  9125  domsdomtrfi  9126  sucdom2  9127  php3  9133  1sdom2dom  9154  sucxpdom  9161  findcard3  9183  isfinite2  9198  card2on  9459  fict  9565  fidomtri2  9909  prdom2  9919  infxpenlem  9926  indcardi  9954  alephnbtwn2  9985  alephsucdom  9992  alephdom  9994  dfac13  10056  djulepw  10106  infdjuabs  10118  infdif  10121  infunsdom1  10125  infunsdom  10126  infxp  10127  cfslb2n  10181  sdom2en01  10215  isfin32i  10278  fin34  10303  fin67  10308  hsmexlem1  10339  hsmex3  10347  entri3  10472  alephexp1  10493  gchdomtri  10543  canthp1  10568  pwfseqlem5  10577  gchdjuidm  10582  gchxpidm  10583  gchpwdom  10584  hargch  10587  gchaclem  10592  gchhar  10593  gchac  10595  inawinalem  10603  inar1  10689  rankcf  10691  tskuni  10697  grothac  10744  rpnnen  16185  rexpen  16186  aleph1irr  16204  dis1stc  23482  hauspwdom  23484  sibfof  34524  ctbssinf  37768  pibt2  37779  heiborlem3  38180  harinf  43479  saluncl  46760  meadjun  46905  meaiunlelem  46911  omeunle  46959