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 8545 | . . . 4 ⊢ ≈ Er V | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → ≈ Er V) |
3 | 2 | ertr 8294 | . 2 ⊢ (⊤ → ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)) |
4 | 3 | mptru 1535 | 1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ⊤wtru 1529 Vcvv 3495 class class class wbr 5058 Er wer 8276 ≈ cen 8495 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-er 8279 df-en 8499 |
This theorem is referenced by: entri 8552 snmapen1 8580 en2sn 8582 xpsnen2g 8599 omxpen 8608 enen1 8646 enen2 8647 map2xp 8676 pwen 8679 ssenen 8680 phplem4 8688 php3 8692 snnen2o 8696 fineqvlem 8721 ssfi 8727 en1eqsn 8737 dif1en 8740 unfi 8774 unxpwdom2 9041 infdifsn 9109 infdiffi 9110 karden 9313 xpnum 9369 cardidm 9377 ficardom 9379 carden2a 9384 carden2b 9385 isinffi 9410 pm54.43 9418 pr2ne 9420 en2eqpr 9422 en2eleq 9423 infxpenlem 9428 infxpidm2 9432 mappwen 9527 finnisoeu 9528 djuen 9584 djuenun 9585 dju1dif 9587 djuassen 9593 mapdjuen 9595 pwdjuen 9596 infdju1 9604 pwdju1 9605 pwdjuidm 9606 cardadju 9609 ficardun 9613 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 13327 hashdvds 16102 unbenlem 16234 unben 16235 4sqlem11 16281 pmtrfconj 18525 psgnunilem1 18552 odinf 18621 dfod2 18622 sylow2blem1 18676 sylow2 18682 simpgnsgd 19153 frlmisfrlm 20922 hmphindis 22335 dyadmbl 24130 fnpreimac 30345 padct 30382 f1ocnt 30452 volmeas 31390 sconnpi1 32384 lzenom 39247 fiphp3d 39296 frlmpwfi 39578 isnumbasgrplem3 39585 fiuneneq 39677 rp-isfinite5 39763 enrelmap 40223 enrelmapr 40224 enmappw 40225 uspgrymrelen 43875 |
Copyright terms: Public domain | W3C validator |