![]() |
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 8539 | . . . 4 ⊢ ≈ Er V | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → ≈ Er V) |
3 | 2 | ertr 8287 | . 2 ⊢ (⊤ → ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)) |
4 | 3 | mptru 1545 | 1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ⊤wtru 1539 Vcvv 3441 class class class wbr 5030 Er wer 8269 ≈ cen 8489 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-er 8272 df-en 8493 |
This theorem is referenced by: entri 8546 snmapen1 8574 en2sn 8576 xpsnen2g 8593 omxpen 8602 enen1 8641 enen2 8642 map2xp 8671 pwen 8674 ssenen 8675 phplem4 8683 php3 8687 snnen2o 8691 fineqvlem 8716 ssfi 8722 en1eqsn 8732 dif1en 8735 unfi 8769 unxpwdom2 9036 infdifsn 9104 infdiffi 9105 karden 9308 xpnum 9364 cardidm 9372 ficardom 9374 carden2a 9379 carden2b 9380 isinffi 9405 pm54.43 9414 pr2ne 9416 en2eqpr 9418 en2eleq 9419 infxpenlem 9424 infxpidm2 9428 mappwen 9523 finnisoeu 9524 djuen 9580 djuenun 9581 dju1dif 9583 djuassen 9589 mapdjuen 9591 pwdjuen 9592 infdju1 9600 pwdju1 9601 pwdjuidm 9602 cardadju 9605 nnadju 9608 ficardadju 9610 ficardun 9611 ficardunOLD 9612 pwsdompw 9615 infxp 9626 infmap2 9629 ackbij1lem5 9635 ackbij1lem9 9639 ackbij1b 9650 fin4en1 9720 isfin4p1 9726 fin23lem23 9737 domtriomlem 9853 axcclem 9868 carden 9962 alephadd 9988 gchdjuidm 10079 gchxpidm 10080 gchpwdom 10081 gchhar 10090 tskuni 10194 fzen2 13332 hashdvds 16102 unbenlem 16234 unben 16235 4sqlem11 16281 pmtrfconj 18586 psgnunilem1 18613 odinf 18682 dfod2 18683 sylow2blem1 18737 sylow2 18743 simpgnsgd 19215 frlmisfrlm 20537 hmphindis 22402 dyadmbl 24204 fnpreimac 30434 padct 30481 f1ocnt 30551 volmeas 31600 sconnpi1 32599 lzenom 39711 fiphp3d 39760 frlmpwfi 40042 isnumbasgrplem3 40049 fiuneneq 40141 rp-isfinite5 40225 enrelmap 40698 enrelmapr 40699 enmappw 40700 uspgrymrelen 44381 |
Copyright terms: Public domain | W3C validator |