Theorem entr 8946

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1543  Vcvv 3430   class class class wbr 5086   Er wer 8633   ≈ cen 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-er 8636  df-en 8887

This theorem is referenced by:  entri  8948  snmapen1  8979  xpsnen2g  9001  omxpen  9010  enen1  9048  enen2  9049  map2xp  9078  pwen  9081  ssenen  9082  ssfiALT  9101  fineqvlem  9169  dif1ennnALT  9180  unxpwdom2  9496  infdifsn  9569  infdiffi  9570  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  10491  gchdjuidm  10582  gchxpidm  10583  gchpwdom  10584  gchhar  10593  tskuni  10697  fzen2  13922  hashdvds  16736  unbenlem  16870  unben  16871  4sqlem11  16917  pmtrfconj  19432  psgnunilem1  19459  odinf  19529  dfod2  19530  sylow2blem1  19586  sylow2  19592  simpgnsgd  20068  frlmisfrlm  21838  hmphindis  23772  dyadmbl  25577  fnpreimac  32758  padct  32806  f1ocnt  32888  volmeas  34391  sconnpi1  35437  lzenom  43216  fiphp3d  43265  frlmpwfi  43544  isnumbasgrplem3  43551  fiuneneq  43638  rp-isfinite5  43962  enrelmap  44442  enrelmapr  44443  enmappw  44444  uspgrymrelen  48641  termcterm2  50001