Theorem sdomdom 8954

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5110   ≈ cen 8918   ≼ cdom 8919   ≺ csdm 8920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-br 5111  df-sdom 8924

This theorem is referenced by:  domdifsn  9028  sucdom2OLD  9056  sdomnsym  9072  sdomdomtr  9080  domsdomtr  9082  sdomtr  9085  domnsymfi  9170  sdomdomtrfi  9171  domsdomtrfi  9172  sucdom2  9173  php3  9179  1sdom2dom  9201  sucxpdom  9209  findcard3  9236  isfinite2  9252  card2on  9514  fict  9613  fidomtri2  9954  prdom2  9966  infxpenlem  9973  indcardi  10001  alephnbtwn2  10032  alephsucdom  10039  alephdom  10041  dfac13  10103  djulepw  10153  infdjuabs  10165  infdif  10168  infunsdom1  10172  infunsdom  10173  infxp  10174  cfslb2n  10228  sdom2en01  10262  isfin32i  10325  fin34  10350  fin67  10355  hsmexlem1  10386  hsmex3  10394  entri3  10519  alephexp1  10539  gchdomtri  10589  canthp1  10614  pwfseqlem5  10623  gchdjuidm  10628  gchxpidm  10629  gchpwdom  10630  hargch  10633  gchaclem  10638  gchhar  10639  gchac  10641  inawinalem  10649  inar1  10735  rankcf  10737  tskuni  10743  grothac  10790  rpnnen  16202  rexpen  16203  aleph1irr  16221  dis1stc  23393  hauspwdom  23395  sibfof  34338  ctbssinf  37401  pibt2  37412  heiborlem3  37814  harinf  43030  saluncl  46322  meadjun  46467  meaiunlelem  46473  omeunle  46521