Theorem sdomdom 8975

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 5148   ≈ cen 8935   ≼ cdom 8936   ≺ csdm 8937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-br 5149  df-sdom 8941

This theorem is referenced by:  domdifsn  9053  sucdom2OLD  9081  sdomnsym  9097  sdomdomtr  9109  domsdomtr  9111  sdomtr  9114  domnsymfi  9202  sdomdomtrfi  9203  domsdomtrfi  9204  sucdom2  9205  php3  9211  1sdom2dom  9246  sucxpdom  9254  findcard3  9284  isfinite2  9300  pwfiOLD  9346  card2on  9548  fict  9647  fidomtri2  9988  prdom2  10000  infxpenlem  10007  indcardi  10035  alephnbtwn2  10066  alephsucdom  10073  alephdom  10075  dfac13  10136  djulepw  10186  infdjuabs  10200  infdif  10203  infunsdom1  10207  infunsdom  10208  infxp  10209  cfslb2n  10262  sdom2en01  10296  isfin32i  10359  fin34  10384  fin67  10389  hsmexlem1  10420  hsmex3  10428  entri3  10553  alephexp1  10573  gchdomtri  10623  canthp1  10648  pwfseqlem5  10657  gchdjuidm  10662  gchxpidm  10663  gchpwdom  10664  hargch  10667  gchaclem  10672  gchhar  10673  gchac  10675  inawinalem  10683  inar1  10769  rankcf  10771  tskuni  10777  grothac  10824  rpnnen  16169  rexpen  16170  aleph1irr  16188  dis1stc  23002  hauspwdom  23004  sibfof  33334  ctbssinf  36282  pibt2  36293  heiborlem3  36676  harinf  41763  saluncl  45023  meadjun  45168  meaiunlelem  45174  omeunle  45222