Theorem sdomdom 7983

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 4653   ≈ cen 7952   ≼ cdom 7953   ≺ csdm 7954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-br 4654  df-sdom 7958

This theorem is referenced by:  domdifsn  8043  sdomnsym  8085  sdomdomtr  8093  domsdomtr  8095  sdomtr  8098  sucdom2  8156  sucxpdom  8169  isfinite2  8218  pwfi  8261  card2on  8459  fict  8550  fidomtri2  8820  prdom2  8829  infxpenlem  8836  indcardi  8864  alephnbtwn2  8895  alephsucdom  8902  alephdom  8904  dfac13  8964  cdalepw  9018  infcdaabs  9028  infdif  9031  infunsdom1  9035  infunsdom  9036  infxp  9037  cfslb2n  9090  sdom2en01  9124  isfin32i  9187  fin34  9212  fin67  9217  hsmexlem1  9248  hsmex3  9256  entri3  9381  unirnfdomd  9389  alephexp1  9401  cfpwsdom  9406  gchdomtri  9451  canthp1  9476  pwfseqlem5  9485  gchcdaidm  9490  gchxpidm  9491  gchpwdom  9492  hargch  9495  gchaclem  9500  gchhar  9501  gchac  9503  inawinalem  9511  inar1  9597  rankcf  9599  tskuni  9605  grothac  9652  rpnnen  14956  rexpen  14957  aleph1irr  14975  dis1stc  21302  hauspwdom  21304  ovolfi  23262  sibfof  30402  heiborlem3  33612  harinf  37601  saluncl  40537  meadjun  40679  meaiunlelem  40685  omeunle  40730