Theorem sdomdom 7869

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 4583   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-br 4584  df-sdom 7844

This theorem is referenced by:  domdifsn  7928  sdomnsym  7970  sdomdomtr  7978  domsdomtr  7980  sdomtr  7983  sucdom2  8041  sucxpdom  8054  isfinite2  8103  pwfi  8144  card2on  8342  fict  8433  fidomtri2  8703  prdom2  8712  infxpenlem  8719  indcardi  8747  alephnbtwn2  8778  alephsucdom  8785  alephdom  8787  dfac13  8847  cdalepw  8901  infcdaabs  8911  infdif  8914  infunsdom1  8918  infunsdom  8919  infxp  8920  cfslb2n  8973  sdom2en01  9007  isfin32i  9070  fin34  9095  fin67  9100  hsmexlem1  9131  hsmex3  9139  entri3  9260  unirnfdomd  9268  alephexp1  9280  cfpwsdom  9285  gchdomtri  9330  canthp1  9355  pwfseqlem5  9364  gchcdaidm  9369  gchxpidm  9370  gchpwdom  9371  hargch  9374  gchaclem  9379  gchhar  9380  gchac  9382  inawinalem  9390  inar1  9476  rankcf  9478  tskuni  9484  grothac  9531  rpnnen  14795  rexpen  14796  aleph1irr  14814  dis1stc  21112  hauspwdom  21114  ovolfi  23069  sibfof  29729  heiborlem3  32782  harinf  36619  saluncl  39213  meadjun  39355  meaiunlelem  39361  omeunle  39406