Theorem entr 8955

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1543  Vcvv 3442   class class class wbr 5100   Er wer 8642   ≈ cen 8892

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 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-er 8645  df-en 8896

This theorem is referenced by:  entri  8957  snmapen1  8988  xpsnen2g  9010  omxpen  9019  enen1  9057  enen2  9058  map2xp  9087  pwen  9090  ssenen  9091  ssfiALT  9110  fineqvlem  9178  dif1ennnALT  9189  unxpwdom2  9505  infdifsn  9578  infdiffi  9579  karden  9819  xpnum  9875  cardidm  9883  ficardom  9885  carden2a  9890  carden2b  9891  isinffi  9916  pm54.43  9925  en2eqpr  9929  en2eleq  9930  infxpenlem  9935  infxpidm2  9939  mappwen  10034  finnisoeu  10035  djuen  10092  djuenun  10093  dju1dif  10095  djuassen  10101  mapdjuen  10103  pwdjuen  10104  infdju1  10112  pwdju1  10113  pwdjuidm  10114  cardadju  10117  nnadju  10120  ficardadju  10122  ficardun  10123  pwsdompw  10125  infxp  10136  infmap2  10139  ackbij1lem5  10145  ackbij1lem9  10149  ackbij1b  10160  fin4en1  10231  isfin4p1  10237  fin23lem23  10248  domtriomlem  10364  axcclem  10379  carden  10473  alephadd  10500  gchdjuidm  10591  gchxpidm  10592  gchpwdom  10593  gchhar  10602  tskuni  10706  fzen2  13904  hashdvds  16714  unbenlem  16848  unben  16849  4sqlem11  16895  pmtrfconj  19407  psgnunilem1  19434  odinf  19504  dfod2  19505  sylow2blem1  19561  sylow2  19567  simpgnsgd  20043  frlmisfrlm  21815  hmphindis  23753  dyadmbl  25569  fnpreimac  32759  padct  32807  f1ocnt  32890  volmeas  34408  sconnpi1  35452  lzenom  43124  fiphp3d  43173  frlmpwfi  43452  isnumbasgrplem3  43459  fiuneneq  43546  rp-isfinite5  43870  enrelmap  44350  enrelmapr  44351  enmappw  44352  uspgrymrelen  48510  termcterm2  49870