Theorem sdomdom 8326

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

Syntax hints:  ¬ wn 3   → wi 4   class class class wbr 4923   ≈ cen 8295   ≼ cdom 8296   ≺ csdm 8297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-dif 3828  df-br 4924  df-sdom 8301

This theorem is referenced by:  domdifsn  8388  sdomnsym  8430  sdomdomtr  8438  domsdomtr  8440  sdomtr  8443  sucdom2  8501  sucxpdom  8514  isfinite2  8563  pwfi  8606  card2on  8805  fict  8902  fidomtri2  9209  prdom2  9218  infxpenlem  9225  indcardi  9253  alephnbtwn2  9284  alephsucdom  9291  alephdom  9293  dfac13  9354  djulepw  9408  infdjuabs  9418  infdif  9421  infunsdom1  9425  infunsdom  9426  infxp  9427  cfslb2n  9480  sdom2en01  9514  isfin32i  9577  fin34  9602  fin67  9607  hsmexlem1  9638  hsmex3  9646  entri3  9771  alephexp1  9791  gchdomtri  9841  canthp1  9866  pwfseqlem5  9875  gchdjuidm  9880  gchxpidm  9881  gchpwdom  9882  hargch  9885  gchaclem  9890  gchhar  9891  gchac  9893  inawinalem  9901  inar1  9987  rankcf  9989  tskuni  9995  grothac  10042  rpnnen  15430  rexpen  15431  aleph1irr  15449  dis1stc  21801  hauspwdom  21803  sibfof  31200  ctbssinf  34063  pibt2  34074  heiborlem3  34481  harinf  38972  saluncl  41979  meadjun  42121  meaiunlelem  42127  omeunle  42175