Theorem sdomdom 9007

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5103   ≈ cen 8970   ≼ cdom 8971   ≺ csdm 8972

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-br 5104  df-sdom 8976

This theorem is used by:  domdifsn  9079  sdomnsym  9121  sdomdomtr  9129  domsdomtr  9131  sdomtr  9134  domnsymfi  9215  sdomdomtrfi  9216  domsdomtrfi  9217  sucdom2  9218  php3  9224  1sdom2dom  9245  sucxpdom  9252  findcard3  9274  isfinite2  9290  card2on  9548  fict  9654  fidomtri2  10075  prdom2  10085  infxpenlem  10092  indcardi  10120  alephnbtwn2  10151  alephsucdom  10158  alephdom  10160  dfac13  10221  djulepw  10271  infdjuabs  10283  infdif  10286  infunsdom1  10290  infunsdom  10291  infxp  10292  cfslb2n  10346  sdom2en01  10380  isfin32i  10443  fin34  10468  fin67  10473  hsmexlem1  10504  hsmex3  10512  entri3  10643  alephexp1  10664  gchdomtri  10714  canthp1  10739  pwfseqlem5  10748  gchdjuidm  10753  gchxpidm  10754  gchpwdom  10755  hargch  10758  gchaclem  10763  gchhar  10764  gchac  10766  inawinalem  10774  inar1  10860  rankcf  10862  tskuni  10868  grothac  10915  rpnnen  16395  rexpen  16396  aleph1irr  16414  dis1stc  23818  hauspwdom  23820  sibfof  34972  ctbssinf  38329  pibt2  38340  heiborlem3  38747  harinf  44040  saluncl  47326  meadjun  47471  meaiunlelem  47477  omeunle  47525