Theorem entr 8937

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1542  Vcvv 3437   class class class wbr 5095   Er wer 8627   ≈ cen 8874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-er 8630  df-en 8878

This theorem is referenced by:  entri  8939  snmapen1  8970  xpsnen2g  8992  omxpen  9001  enen1  9039  enen2  9040  map2xp  9069  pwen  9072  ssenen  9073  ssfiALT  9092  fineqvlem  9159  dif1ennnALT  9170  unxpwdom2  9483  infdifsn  9556  infdiffi  9557  karden  9797  xpnum  9853  cardidm  9861  ficardom  9863  carden2a  9868  carden2b  9869  isinffi  9894  pm54.43  9903  en2eqpr  9907  en2eleq  9908  infxpenlem  9913  infxpidm2  9917  mappwen  10012  finnisoeu  10013  djuen  10070  djuenun  10071  dju1dif  10073  djuassen  10079  mapdjuen  10081  pwdjuen  10082  infdju1  10090  pwdju1  10091  pwdjuidm  10092  cardadju  10095  nnadju  10098  ficardadju  10100  ficardun  10101  pwsdompw  10103  infxp  10114  infmap2  10117  ackbij1lem5  10123  ackbij1lem9  10127  ackbij1b  10138  fin4en1  10209  isfin4p1  10215  fin23lem23  10226  domtriomlem  10342  axcclem  10357  carden  10451  alephadd  10477  gchdjuidm  10568  gchxpidm  10569  gchpwdom  10570  gchhar  10579  tskuni  10683  fzen2  13880  hashdvds  16690  unbenlem  16824  unben  16825  4sqlem11  16871  pmtrfconj  19382  psgnunilem1  19409  odinf  19479  dfod2  19480  sylow2blem1  19536  sylow2  19542  simpgnsgd  20018  frlmisfrlm  21789  hmphindis  23715  dyadmbl  25531  fnpreimac  32657  padct  32707  f1ocnt  32789  volmeas  34267  sconnpi1  35306  lzenom  42890  fiphp3d  42939  frlmpwfi  43218  isnumbasgrplem3  43225  fiuneneq  43312  rp-isfinite5  43637  enrelmap  44117  enrelmapr  44118  enmappw  44119  uspgrymrelen  48280  termcterm2  49642