Theorem entr 9005

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ⊤wtru 1571  Vcvv 3457   class class class wbr 5111   Er wer 8693   ≈ cen 8942

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pow 5338  ax-pr 5406  ax-un 7738

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-er 8696  df-en 8946

This theorem is used by:  entri  9007  snmapen1  9039  xpsnen2g  9061  omxpen  9070  enen1  9108  enen2  9109  map2xp  9138  pwen  9141  ssenen  9142  ssfiALT  9161  fineqvlem  9229  dif1ennnALT  9240  unxpwdom2  9553  infdifsn  9629  infdiffi  9630  karden  9891  kardenOLD  9892  xpnum  9949  cardidm  9957  ficardom  9959  carden2a  9964  carden2b  9965  isinffi  9990  pm54.43  9999  en2eqpr  10003  en2eleq  10004  infxpenlem  10009  infxpidm2  10013  mappwen  10108  finnisoeu  10109  djuen  10165  djuenun  10166  dju1dif  10168  djuassen  10174  mapdjuen  10176  pwdjuen  10177  infdju1  10185  pwdju1  10186  pwdjuidm  10187  cardadju  10190  nnadju  10193  ficardadju  10195  ficardun  10196  pwsdompw  10198  infxp  10209  infmap2  10212  ackbij1lem5  10218  ackbij1lem9  10222  ackbij1b  10233  fin4en1  10304  isfin4p1  10310  fin23lem23  10321  domtriomlem  10437  axcclem  10452  carden  10546  alephadd  10573  gchdjuidm  10664  gchxpidm  10665  gchpwdom  10666  gchhar  10675  tskuni  10779  fzen2  14018  hashdvds  16851  unbenlem  16985  unben  16986  4sqlem11  17032  pmtrfconj  19559  psgnunilem1  19586  odinf  19656  dfod2  19657  sylow2blem1  19713  sylow2  19719  simpgnsgd  20195  frlmisfrlm  22027  hmphindis  23983  dyadmbl  25788  fnpreimac  33044  padct  33092  f1ocnt  33174  volmeas  34645  kardexen  35592  sconnpi1  35744  lzenom  43534  fiphp3d  43579  frlmpwfi  43858  isnumbasgrplem3  43865  fiuneneq  43952  rp-isfinite5  44276  enrelmap  44756  enrelmapr  44757  enmappw  44758  uspgrymrelen  48951  termcterm2  50325