Theorem sdomdom 8723

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5070   ≈ cen 8688   ≼ cdom 8689   ≺ csdm 8690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-br 5071  df-sdom 8694

This theorem is referenced by:  domdifsn  8795  sucdom2  8822  sdomnsym  8838  sdomdomtr  8846  domsdomtr  8848  sdomtr  8851  sucxpdom  8961  isfinite2  9002  pwfiOLD  9044  card2on  9243  fict  9341  fidomtri2  9683  prdom2  9693  infxpenlem  9700  indcardi  9728  alephnbtwn2  9759  alephsucdom  9766  alephdom  9768  dfac13  9829  djulepw  9879  infdjuabs  9893  infdif  9896  infunsdom1  9900  infunsdom  9901  infxp  9902  cfslb2n  9955  sdom2en01  9989  isfin32i  10052  fin34  10077  fin67  10082  hsmexlem1  10113  hsmex3  10121  entri3  10246  alephexp1  10266  gchdomtri  10316  canthp1  10341  pwfseqlem5  10350  gchdjuidm  10355  gchxpidm  10356  gchpwdom  10357  hargch  10360  gchaclem  10365  gchhar  10366  gchac  10368  inawinalem  10376  inar1  10462  rankcf  10464  tskuni  10470  grothac  10517  rpnnen  15864  rexpen  15865  aleph1irr  15883  dis1stc  22558  hauspwdom  22560  sibfof  32207  ctbssinf  35504  pibt2  35515  heiborlem3  35898  harinf  40772  saluncl  43748  meadjun  43890  meaiunlelem  43896  omeunle  43944