![]() |
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 8321 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) | |
2 | 1 | simplbi 490 | 1 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |