Theorem entr 9037

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ⊤wtru 1570  Vcvv 3450   class class class wbr 5102   Er wer 8718   ≈ cen 8974

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-er 8721  df-en 8978

This theorem is used by:  entri  9039  snmapen1  9071  xpsnen2g  9093  omxpen  9102  enen1  9140  enen2  9141  map2xp  9170  pwen  9173  ssenen  9174  ssfiALT  9193  fineqvlem  9261  dif1ennnALT  9272  unxpwdom2  9586  infdifsn  9662  infdiffi  9663  karden  9963  kardenOLD  9964  xpnum  10036  cardidm  10044  ficardom  10046  carden2a  10051  carden2b  10052  isinffi  10077  pm54.43  10086  en2eqpr  10090  en2eleq  10091  infxpenlem  10096  infxpidm2  10100  mappwen  10195  finnisoeu  10196  djuen  10252  djuenun  10253  dju1dif  10255  djuassen  10261  mapdjuen  10263  pwdjuen  10264  infdju1  10272  pwdju1  10273  pwdjuidm  10274  cardadju  10277  nnadju  10280  ficardadju  10282  ficardun  10283  pwsdompw  10285  infxp  10296  infmap2  10299  ackbij1lem5  10305  ackbij1lem9  10309  ackbij1b  10320  fin4en1  10391  isfin4p1  10397  fin23lem23  10408  domtriomlem  10524  axcclem  10539  carden  10639  alephadd  10666  gchdjuidm  10757  gchxpidm  10758  gchpwdom  10759  gchhar  10768  tskuni  10872  fzen2  14116  hashdvds  16958  unbenlem  17092  unben  17093  4sqlem11  17139  pmtrfconj  19686  psgnunilem1  19713  odinf  19783  dfod2  19784  sylow2blem1  19840  sylow2  19846  simpgnsgd  20322  frlmisfrlm  22160  hmphindis  24122  dyadmbl  25927  fnpreimac  33312  padct  33358  f1ocnt  33439  volmeas  34911  kardexen  35888  sconnpi1  36091  lzenom  43875  fiphp3d  43920  frlmpwfi  44194  isnumbasgrplem3  44201  fiuneneq  44288  rp-isfinite5  44612  enrelmap  45091  enrelmapr  45092  enmappw  45093  uspgrymrelen  49345  termcterm2  50743