Theorem entr 8980

Description: Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)

Assertion

Ref	Expression
entr	⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)

Proof of Theorem entr

Step	Hyp	Ref	Expression
1		ener 8975	. . . 4 ⊢ ≈ Er V
2	1	a1i 11	. . 3 ⊢ (⊤ → ≈ Er V)
3	2	ertr 8687	. 2 ⊢ (⊤ → ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶))
4	3	mptru 1566	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399  ⊤wtru 1560  Vcvv 3453   class class class wbr 5097   Er wer 8668   ≈ cen 8917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pow 5319  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-er 8671  df-en 8921

This theorem is referenced by:  entri  8982  snmapen1  9013  xpsnen2g  9035  omxpen  9044  enen1  9082  enen2  9083  map2xp  9112  pwen  9115  ssenen  9116  ssfiALT  9135  fineqvlem  9203  dif1ennnALT  9214  unxpwdom2  9529  infdifsn  9605  infdiffi  9606  karden  9846  xpnum  9902  cardidm  9910  ficardom  9912  carden2a  9917  carden2b  9918  isinffi  9943  pm54.43  9952  en2eqpr  9956  en2eleq  9957  infxpenlem  9962  infxpidm2  9966  mappwen  10061  finnisoeu  10062  djuen  10119  djuenun  10120  dju1dif  10122  djuassen  10128  mapdjuen  10130  pwdjuen  10131  infdju1  10139  pwdju1  10140  pwdjuidm  10141  cardadju  10144  nnadju  10147  ficardadju  10149  ficardun  10150  pwsdompw  10152  infxp  10163  infmap2  10166  ackbij1lem5  10172  ackbij1lem9  10176  ackbij1b  10187  fin4en1  10259  isfin4p1  10265  fin23lem23  10276  domtriomlem  10392  axcclem  10407  carden  10501  alephadd  10528  gchdjuidm  10619  gchxpidm  10620  gchpwdom  10621  gchhar  10630  tskuni  10734  fzen2  13975  hashdvds  16800  unbenlem  16934  unben  16935  4sqlem11  16981  pmtrfconj  19496  psgnunilem1  19523  odinf  19593  dfod2  19594  sylow2blem1  19650  sylow2  19656  simpgnsgd  20132  frlmisfrlm  21887  hmphindis  23844  dyadmbl  25649  fnpreimac  32832  padct  32880  f1ocnt  32962  volmeas  34488  sconnpi1  35549  lzenom  43311  fiphp3d  43356  frlmpwfi  43635  isnumbasgrplem3  43642  fiuneneq  43729  rp-isfinite5  44053  enrelmap  44533  enrelmapr  44534  enmappw  44535  uspgrymrelen  48735  termcterm2  50095