Theorem entr 8953

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1543  Vcvv 3429   class class class wbr 5085   Er wer 8640   ≈ cen 8890

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 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-er 8643  df-en 8894

This theorem is referenced by:  entri  8955  snmapen1  8986  xpsnen2g  9008  omxpen  9017  enen1  9055  enen2  9056  map2xp  9085  pwen  9088  ssenen  9089  ssfiALT  9108  fineqvlem  9176  dif1ennnALT  9187  unxpwdom2  9503  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  13931  hashdvds  16745  unbenlem  16879  unben  16880  4sqlem11  16926  pmtrfconj  19441  psgnunilem1  19468  odinf  19538  dfod2  19539  sylow2blem1  19595  sylow2  19601  simpgnsgd  20077  frlmisfrlm  21828  hmphindis  23762  dyadmbl  25567  fnpreimac  32743  padct  32791  f1ocnt  32873  volmeas  34375  sconnpi1  35421  lzenom  43202  fiphp3d  43247  frlmpwfi  43526  isnumbasgrplem3  43533  fiuneneq  43620  rp-isfinite5  43944  enrelmap  44424  enrelmapr  44425  enmappw  44426  uspgrymrelen  48629  termcterm2  49989