![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > entr | Structured version Visualization version GIF version |
Description: Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.) |
Ref | Expression |
---|---|
entr | ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ener 9022 | . . . 4 ⊢ ≈ Er V | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → ≈ Er V) |
3 | 2 | ertr 8740 | . 2 ⊢ (⊤ → ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)) |
4 | 3 | mptru 1540 | 1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ⊤wtru 1534 Vcvv 3461 class class class wbr 5149 Er wer 8722 ≈ cen 8961 |
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-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 |
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 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-er 8725 df-en 8965 |
This theorem is referenced by: entri 9029 snmapen1 9064 en2snOLDOLD 9068 xpsnen2g 9090 omxpen 9099 enen1 9142 enen2 9143 map2xp 9172 pwen 9175 ssenen 9176 ssfiALT 9199 phplem4OLD 9245 php3OLD 9249 snnen2oOLD 9252 fineqvlem 9287 en1eqsnOLD 9300 dif1ennnALT 9302 unfiOLD 9338 unxpwdom2 9613 infdifsn 9682 infdiffi 9683 karden 9920 xpnum 9976 cardidm 9984 ficardom 9986 carden2a 9991 carden2b 9992 isinffi 10017 pm54.43 10026 pr2neOLD 10030 en2eqpr 10032 en2eleq 10033 infxpenlem 10038 infxpidm2 10042 mappwen 10137 finnisoeu 10138 djuen 10194 djuenun 10195 dju1dif 10197 djuassen 10203 mapdjuen 10205 pwdjuen 10206 infdju1 10214 pwdju1 10215 pwdjuidm 10216 cardadju 10219 nnadju 10222 ficardadju 10224 ficardun 10225 ficardunOLD 10226 pwsdompw 10229 infxp 10240 infmap2 10243 ackbij1lem5 10249 ackbij1lem9 10253 ackbij1b 10264 fin4en1 10334 isfin4p1 10340 fin23lem23 10351 domtriomlem 10467 axcclem 10482 carden 10576 alephadd 10602 gchdjuidm 10693 gchxpidm 10694 gchpwdom 10695 gchhar 10704 tskuni 10808 fzen2 13970 hashdvds 16747 unbenlem 16880 unben 16881 4sqlem11 16927 pmtrfconj 19433 psgnunilem1 19460 odinf 19530 dfod2 19531 sylow2blem1 19587 sylow2 19593 simpgnsgd 20069 frlmisfrlm 21799 hmphindis 23745 dyadmbl 25573 fnpreimac 32538 padct 32583 f1ocnt 32652 volmeas 33981 sconnpi1 34980 lzenom 42332 fiphp3d 42381 frlmpwfi 42664 isnumbasgrplem3 42671 fiuneneq 42762 rp-isfinite5 43089 enrelmap 43569 enrelmapr 43570 enmappw 43571 uspgrymrelen 47401 |
Copyright terms: Public domain | W3C validator |