![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > endom | Structured version Visualization version GIF version |
Description: Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.) |
Ref | Expression |
---|---|
endom | ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enssdom 9004 | . 2 ⊢ ≈ ⊆ ≼ | |
2 | 1 | ssbri 5197 | 1 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 class class class wbr 5152 ≈ cen 8967 ≼ cdom 8968 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-12 2166 ax-ext 2699 ax-sep 5303 ax-nul 5310 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3431 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-br 5153 df-opab 5215 df-xp 5688 df-rel 5689 df-f1o 6560 df-en 8971 df-dom 8972 |
This theorem is referenced by: bren2 9010 domrefg 9014 endomtr 9039 domentr 9040 domunsncan 9103 sbthb 9125 dom0 9133 sdomentr 9142 ensdomtr 9144 domtriord 9154 domunsn 9158 xpen 9171 sdomdomtrfi 9235 domsdomtrfi 9236 sucdom2 9237 php 9241 php3 9243 onomeneq 9259 0sdom1dom 9269 rex2dom 9277 unxpdom2 9285 sucxpdom 9286 f1finf1o 9302 findcard3 9316 wdomen1 9607 wdomen2 9608 fidomtri2 10025 prdom2 10037 acnen 10084 acnen2 10086 alephdom 10112 alephinit 10126 undjudom 10198 pwdjudom 10247 fin1a2lem11 10441 hsmexlem1 10457 gchdomtri 10660 gchdjuidm 10699 gchxpidm 10700 gchpwdom 10701 gchhar 10710 gruina 10849 nnct 13986 odinf 19525 hauspwdom 23425 ufildom1 23850 iscmet3 25241 mbfaddlem 25609 ctbssinf 36918 pibt2 36929 heiborlem3 37319 zct 44456 qct 44773 caratheodory 45945 |
Copyright terms: Public domain | W3C validator |