Theorem entr 9026

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ⊤wtru 1571  Vcvv 3451   class class class wbr 5103   Er wer 8707   ≈ cen 8963

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-er 8710  df-en 8967

This theorem is used by:  entri  9028  snmapen1  9060  xpsnen2g  9082  omxpen  9091  enen1  9129  enen2  9130  map2xp  9159  pwen  9162  ssenen  9163  ssfiALT  9182  fineqvlem  9250  dif1ennnALT  9261  unxpwdom2  9575  infdifsn  9651  infdiffi  9652  karden  9952  kardenOLD  9953  xpnum  10025  cardidm  10033  ficardom  10035  carden2a  10040  carden2b  10041  isinffi  10066  pm54.43  10075  en2eqpr  10079  en2eleq  10080  infxpenlem  10085  infxpidm2  10089  mappwen  10184  finnisoeu  10185  djuen  10241  djuenun  10242  dju1dif  10244  djuassen  10250  mapdjuen  10252  pwdjuen  10253  infdju1  10261  pwdju1  10262  pwdjuidm  10263  cardadju  10266  nnadju  10269  ficardadju  10271  ficardun  10272  pwsdompw  10274  infxp  10285  infmap2  10288  ackbij1lem5  10294  ackbij1lem9  10298  ackbij1b  10309  fin4en1  10380  isfin4p1  10386  fin23lem23  10397  domtriomlem  10513  axcclem  10528  carden  10628  alephadd  10655  gchdjuidm  10746  gchxpidm  10747  gchpwdom  10748  gchhar  10757  tskuni  10861  fzen2  14105  hashdvds  16945  unbenlem  17079  unben  17080  4sqlem11  17126  pmtrfconj  19673  psgnunilem1  19700  odinf  19770  dfod2  19771  sylow2blem1  19827  sylow2  19833  simpgnsgd  20309  frlmisfrlm  22147  hmphindis  24109  dyadmbl  25914  fnpreimac  33257  padct  33303  f1ocnt  33385  volmeas  34857  kardexen  35814  sconnpi1  35983  lzenom  43760  fiphp3d  43805  frlmpwfi  44084  isnumbasgrplem3  44091  fiuneneq  44178  rp-isfinite5  44502  enrelmap  44982  enrelmapr  44983  enmappw  44984  uspgrymrelen  49220  termcterm2  50591