Theorem entr 9027

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

Syntax hints:   → wi 4   ∧ wa 394  ⊤wtru 1534  Vcvv 3461   class class class wbr 5149   Er wer 8722   ≈ cen 8961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-er 8725  df-en 8965

This theorem is referenced by:  entri  9029  snmapen1  9064  en2snOLDOLD  9068  xpsnen2g  9090  omxpen  9099  enen1  9142  enen2  9143  map2xp  9172  pwen  9175  ssenen  9176  ssfiALT  9199  phplem4OLD  9245  php3OLD  9249  snnen2oOLD  9252  fineqvlem  9287  en1eqsnOLD  9300  dif1ennnALT  9302  unfiOLD  9338  unxpwdom2  9613  infdifsn  9682  infdiffi  9683  karden  9920  xpnum  9976  cardidm  9984  ficardom  9986  carden2a  9991  carden2b  9992  isinffi  10017  pm54.43  10026  pr2neOLD  10030  en2eqpr  10032  en2eleq  10033  infxpenlem  10038  infxpidm2  10042  mappwen  10137  finnisoeu  10138  djuen  10194  djuenun  10195  dju1dif  10197  djuassen  10203  mapdjuen  10205  pwdjuen  10206  infdju1  10214  pwdju1  10215  pwdjuidm  10216  cardadju  10219  nnadju  10222  ficardadju  10224  ficardun  10225  ficardunOLD  10226  pwsdompw  10229  infxp  10240  infmap2  10243  ackbij1lem5  10249  ackbij1lem9  10253  ackbij1b  10264  fin4en1  10334  isfin4p1  10340  fin23lem23  10351  domtriomlem  10467  axcclem  10482  carden  10576  alephadd  10602  gchdjuidm  10693  gchxpidm  10694  gchpwdom  10695  gchhar  10704  tskuni  10808  fzen2  13970  hashdvds  16747  unbenlem  16880  unben  16881  4sqlem11  16927  pmtrfconj  19433  psgnunilem1  19460  odinf  19530  dfod2  19531  sylow2blem1  19587  sylow2  19593  simpgnsgd  20069  frlmisfrlm  21799  hmphindis  23745  dyadmbl  25573  fnpreimac  32538  padct  32583  f1ocnt  32652  volmeas  33981  sconnpi1  34980  lzenom  42332  fiphp3d  42381  frlmpwfi  42664  isnumbasgrplem3  42671  fiuneneq  42762  rp-isfinite5  43089  enrelmap  43569  enrelmapr  43570  enmappw  43571  uspgrymrelen  47401