Theorem entr 8938

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 8933	. . . 4 ⊢ ≈ Er V
2	1	a1i 11	. . 3 ⊢ (⊤ → ≈ Er V)
3	2	ertr 8647	. 2 ⊢ (⊤ → ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶))
4	3	mptru 1547	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1541  Vcvv 3438   class class class wbr 5095   Er wer 8629   ≈ cen 8876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-er 8632  df-en 8880

This theorem is referenced by:  entri  8940  snmapen1  8971  xpsnen2g  8994  omxpen  9003  enen1  9041  enen2  9042  map2xp  9071  pwen  9074  ssenen  9075  ssfiALT  9098  fineqvlem  9167  en1eqsnOLD  9178  dif1ennnALT  9180  unxpwdom2  9499  infdifsn  9572  infdiffi  9573  karden  9810  xpnum  9866  cardidm  9874  ficardom  9876  carden2a  9881  carden2b  9882  isinffi  9907  pm54.43  9916  en2eqpr  9920  en2eleq  9921  infxpenlem  9926  infxpidm2  9930  mappwen  10025  finnisoeu  10026  djuen  10083  djuenun  10084  dju1dif  10086  djuassen  10092  mapdjuen  10094  pwdjuen  10095  infdju1  10103  pwdju1  10104  pwdjuidm  10105  cardadju  10108  nnadju  10111  ficardadju  10113  ficardun  10114  pwsdompw  10116  infxp  10127  infmap2  10130  ackbij1lem5  10136  ackbij1lem9  10140  ackbij1b  10151  fin4en1  10222  isfin4p1  10228  fin23lem23  10239  domtriomlem  10355  axcclem  10370  carden  10464  alephadd  10490  gchdjuidm  10581  gchxpidm  10582  gchpwdom  10583  gchhar  10592  tskuni  10696  fzen2  13894  hashdvds  16704  unbenlem  16838  unben  16839  4sqlem11  16885  pmtrfconj  19363  psgnunilem1  19390  odinf  19460  dfod2  19461  sylow2blem1  19517  sylow2  19523  simpgnsgd  19999  frlmisfrlm  21773  hmphindis  23700  dyadmbl  25517  fnpreimac  32628  padct  32676  f1ocnt  32758  volmeas  34200  sconnpi1  35214  lzenom  42746  fiphp3d  42795  frlmpwfi  43074  isnumbasgrplem3  43081  fiuneneq  43168  rp-isfinite5  43493  enrelmap  43973  enrelmapr  43974  enmappw  43975  uspgrymrelen  48141  termcterm2  49503