![]() |
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 8290 | . . . 4 ⊢ ≈ Er V | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → ≈ Er V) |
3 | 2 | ertr 8043 | . 2 ⊢ (⊤ → ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)) |
4 | 3 | mptru 1609 | 1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ⊤wtru 1602 Vcvv 3398 class class class wbr 4888 Er wer 8025 ≈ cen 8240 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-er 8028 df-en 8244 |
This theorem is referenced by: entri 8297 snmapen1 8325 en2sn 8327 xpsnen2g 8343 omxpen 8352 enen1 8390 enen2 8391 map2xp 8420 pwen 8423 ssenen 8424 phplem4 8432 php3 8436 snnen2o 8439 fineqvlem 8464 ssfi 8470 en1eqsn 8480 dif1en 8483 unfi 8517 unxpwdom2 8784 infdifsn 8853 infdiffi 8854 karden 9057 xpnum 9112 cardidm 9120 ficardom 9122 carden2a 9127 carden2b 9128 isinffi 9153 pm54.43 9161 pr2ne 9163 en2eqpr 9165 en2eleq 9166 infxpenlem 9171 infxpidm2 9175 mappwen 9270 finnisoeu 9271 cdaen 9332 cdaenun 9333 cda1dif 9335 cdaassen 9341 mapcdaen 9343 pwcdaen 9344 infcda1 9352 pwcdaidm 9354 cardacda 9357 ficardun 9361 pwsdompw 9363 infxp 9374 infmap2 9377 ackbij1lem5 9383 ackbij1lem9 9387 ackbij1b 9398 fin4en1 9468 isfin4-3 9474 fin23lem23 9485 domtriomlem 9601 axcclem 9616 carden 9710 alephadd 9736 gchcdaidm 9827 gchxpidm 9828 gchpwdom 9829 gchhar 9838 tskuni 9942 fzen2 13091 hashdvds 15888 unbenlem 16020 unben 16021 4sqlem11 16067 pmtrfconj 18273 psgnunilem1 18300 odinf 18368 dfod2 18369 sylow2blem1 18423 sylow2 18429 frlmisfrlm 20595 hmphindis 22013 dyadmbl 23808 fnpreimac 30040 padct 30067 f1ocnt 30127 volmeas 30896 sconnpi1 31824 lzenom 38303 fiphp3d 38353 frlmpwfi 38637 isnumbasgrplem3 38644 fiuneneq 38744 rp-isfinite5 38830 enrelmap 39257 enrelmapr 39258 enmappw 39259 uspgrymrelen 42786 |
Copyright terms: Public domain | W3C validator |