Theorem entr 8928

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1542  Vcvv 3436   class class class wbr 5091   Er wer 8619   ≈ cen 8866

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-er 8622  df-en 8870

This theorem is referenced by:  entri  8930  snmapen1  8961  xpsnen2g  8983  omxpen  8992  enen1  9030  enen2  9031  map2xp  9060  pwen  9063  ssenen  9064  ssfiALT  9083  fineqvlem  9150  dif1ennnALT  9161  unxpwdom2  9474  infdifsn  9547  infdiffi  9548  karden  9788  xpnum  9844  cardidm  9852  ficardom  9854  carden2a  9859  carden2b  9860  isinffi  9885  pm54.43  9894  en2eqpr  9898  en2eleq  9899  infxpenlem  9904  infxpidm2  9908  mappwen  10003  finnisoeu  10004  djuen  10061  djuenun  10062  dju1dif  10064  djuassen  10070  mapdjuen  10072  pwdjuen  10073  infdju1  10081  pwdju1  10082  pwdjuidm  10083  cardadju  10086  nnadju  10089  ficardadju  10091  ficardun  10092  pwsdompw  10094  infxp  10105  infmap2  10108  ackbij1lem5  10114  ackbij1lem9  10118  ackbij1b  10129  fin4en1  10200  isfin4p1  10206  fin23lem23  10217  domtriomlem  10333  axcclem  10348  carden  10442  alephadd  10468  gchdjuidm  10559  gchxpidm  10560  gchpwdom  10561  gchhar  10570  tskuni  10674  fzen2  13876  hashdvds  16686  unbenlem  16820  unben  16821  4sqlem11  16867  pmtrfconj  19379  psgnunilem1  19406  odinf  19476  dfod2  19477  sylow2blem1  19533  sylow2  19539  simpgnsgd  20015  frlmisfrlm  21786  hmphindis  23713  dyadmbl  25529  fnpreimac  32651  padct  32699  f1ocnt  32780  volmeas  34242  sconnpi1  35281  lzenom  42809  fiphp3d  42858  frlmpwfi  43137  isnumbasgrplem3  43144  fiuneneq  43231  rp-isfinite5  43556  enrelmap  44036  enrelmapr  44037  enmappw  44038  uspgrymrelen  48190  termcterm2  49552