![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sdomdom | Structured version Visualization version GIF version |
Description: Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.) |
Ref | Expression |
---|---|
sdomdom | ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brsdom 8995 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) | |
2 | 1 | simplbi 496 | 1 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 class class class wbr 5143 ≈ cen 8960 ≼ cdom 8961 ≺ csdm 8962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-dif 3949 df-br 5144 df-sdom 8966 |
This theorem is referenced by: domdifsn 9081 sucdom2OLD 9109 sdomnsym 9125 sdomdomtr 9137 domsdomtr 9139 sdomtr 9142 domnsymfi 9227 sdomdomtrfi 9228 domsdomtrfi 9229 sucdom2 9230 php3 9236 1sdom2dom 9271 sucxpdom 9279 findcard3 9309 isfinite2 9325 pwfiOLD 9381 card2on 9587 fict 9686 fidomtri2 10027 prdom2 10039 infxpenlem 10046 indcardi 10074 alephnbtwn2 10105 alephsucdom 10112 alephdom 10114 dfac13 10175 djulepw 10225 infdjuabs 10237 infdif 10240 infunsdom1 10244 infunsdom 10245 infxp 10246 cfslb2n 10299 sdom2en01 10333 isfin32i 10396 fin34 10421 fin67 10426 hsmexlem1 10457 hsmex3 10465 entri3 10590 alephexp1 10610 gchdomtri 10660 canthp1 10685 pwfseqlem5 10694 gchdjuidm 10699 gchxpidm 10700 gchpwdom 10701 hargch 10704 gchaclem 10709 gchhar 10710 gchac 10712 inawinalem 10720 inar1 10806 rankcf 10808 tskuni 10814 grothac 10861 rpnnen 16221 rexpen 16222 aleph1irr 16240 dis1stc 23488 hauspwdom 23490 sibfof 34184 ctbssinf 37123 pibt2 37134 heiborlem3 37524 harinf 42726 saluncl 45971 meadjun 46116 meaiunlelem 46122 omeunle 46170 |
Copyright terms: Public domain | W3C validator |