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 8544 | . . . 4 ⊢ ≈ Er V | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → ≈ Er V) |
3 | 2 | ertr 8293 | . 2 ⊢ (⊤ → ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)) |
4 | 3 | mptru 1535 | 1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ⊤wtru 1529 Vcvv 3492 class class class wbr 5057 Er wer 8275 ≈ cen 8494 |
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 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 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 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-er 8278 df-en 8498 |
This theorem is referenced by: entri 8551 snmapen1 8579 en2sn 8581 xpsnen2g 8598 omxpen 8607 enen1 8645 enen2 8646 map2xp 8675 pwen 8678 ssenen 8679 phplem4 8687 php3 8691 snnen2o 8695 fineqvlem 8720 ssfi 8726 en1eqsn 8736 dif1en 8739 unfi 8773 unxpwdom2 9040 infdifsn 9108 infdiffi 9109 karden 9312 xpnum 9368 cardidm 9376 ficardom 9378 carden2a 9383 carden2b 9384 isinffi 9409 pm54.43 9417 pr2ne 9419 en2eqpr 9421 en2eleq 9422 infxpenlem 9427 infxpidm2 9431 mappwen 9526 finnisoeu 9527 djuen 9583 djuenun 9584 dju1dif 9586 djuassen 9592 mapdjuen 9594 pwdjuen 9595 infdju1 9603 pwdju1 9604 pwdjuidm 9605 cardadju 9608 ficardun 9612 pwsdompw 9614 infxp 9625 infmap2 9628 ackbij1lem5 9634 ackbij1lem9 9638 ackbij1b 9649 fin4en1 9719 isfin4p1 9725 fin23lem23 9736 domtriomlem 9852 axcclem 9867 carden 9961 alephadd 9987 gchdjuidm 10078 gchxpidm 10079 gchpwdom 10080 gchhar 10089 tskuni 10193 fzen2 13325 hashdvds 16100 unbenlem 16232 unben 16233 4sqlem11 16279 pmtrfconj 18523 psgnunilem1 18550 odinf 18619 dfod2 18620 sylow2blem1 18674 sylow2 18680 simpgnsgd 19151 frlmisfrlm 20920 hmphindis 22333 dyadmbl 24128 fnpreimac 30344 padct 30381 f1ocnt 30451 volmeas 31389 sconnpi1 32383 lzenom 39245 fiphp3d 39294 frlmpwfi 39576 isnumbasgrplem3 39583 fiuneneq 39675 rp-isfinite5 39761 enrelmap 40221 enrelmapr 40222 enmappw 40223 uspgrymrelen 43905 |
Copyright terms: Public domain | W3C validator |