Theorem sdomdom 8137

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 4786   ≈ cen 8106   ≼ cdom 8107   ≺ csdm 8108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-br 4787  df-sdom 8112

This theorem is referenced by:  domdifsn  8199  sdomnsym  8241  sdomdomtr  8249  domsdomtr  8251  sdomtr  8254  sucdom2  8312  sucxpdom  8325  isfinite2  8374  pwfi  8417  card2on  8615  fict  8714  fidomtri2  9020  prdom2  9029  infxpenlem  9036  indcardi  9064  alephnbtwn2  9095  alephsucdom  9102  alephdom  9104  dfac13  9166  cdalepw  9220  infcdaabs  9230  infdif  9233  infunsdom1  9237  infunsdom  9238  infxp  9239  cfslb2n  9292  sdom2en01  9326  isfin32i  9389  fin34  9414  fin67  9419  hsmexlem1  9450  hsmex3  9458  entri3  9583  unirnfdomd  9591  alephexp1  9603  cfpwsdom  9608  gchdomtri  9653  canthp1  9678  pwfseqlem5  9687  gchcdaidm  9692  gchxpidm  9693  gchpwdom  9694  hargch  9697  gchaclem  9702  gchhar  9703  gchac  9705  inawinalem  9713  inar1  9799  rankcf  9801  tskuni  9807  grothac  9854  rpnnen  15162  rexpen  15163  aleph1irr  15181  dis1stc  21523  hauspwdom  21525  ovolfi  23482  sibfof  30742  heiborlem3  33944  harinf  38127  saluncl  41054  meadjun  41196  meaiunlelem  41202  omeunle  41250