Theorem sdomdom 8987

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   class class class wbr 5103   ≈ cen 8950   ≼ cdom 8951   ≺ csdm 8952

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-br 5104  df-sdom 8956

This theorem is used by:  domdifsn  9059  sdomnsym  9101  sdomdomtr  9109  domsdomtr  9111  sdomtr  9114  domnsymfi  9195  sdomdomtrfi  9196  domsdomtrfi  9197  sucdom2  9198  php3  9204  1sdom2dom  9225  sucxpdom  9232  findcard3  9254  isfinite2  9269  card2on  9527  fict  9633  fidomtri2  10000  prdom2  10010  infxpenlem  10017  indcardi  10045  alephnbtwn2  10076  alephsucdom  10083  alephdom  10085  dfac13  10146  djulepw  10196  infdjuabs  10208  infdif  10211  infunsdom1  10215  infunsdom  10216  infxp  10217  cfslb2n  10271  sdom2en01  10305  isfin32i  10368  fin34  10393  fin67  10398  hsmexlem1  10429  hsmex3  10437  entri3  10568  alephexp1  10589  gchdomtri  10639  canthp1  10664  pwfseqlem5  10673  gchdjuidm  10678  gchxpidm  10679  gchpwdom  10680  hargch  10683  gchaclem  10688  gchhar  10689  gchac  10691  inawinalem  10699  inar1  10785  rankcf  10787  tskuni  10793  grothac  10840  rpnnen  16316  rexpen  16317  aleph1irr  16335  dis1stc  23726  hauspwdom  23728  sibfof  34852  ctbssinf  38161  pibt2  38172  heiborlem3  38564  harinf  43876  saluncl  47146  meadjun  47291  meaiunlelem  47297  omeunle  47345