Theorem entr 8563

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

Syntax hints:   → wi 4   ∧ wa 398  ⊤wtru 1538  Vcvv 3496   class class class wbr 5068   Er wer 8288   ≈ cen 8508

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-er 8291  df-en 8512

This theorem is referenced by:  entri  8565  snmapen1  8593  en2sn  8595  xpsnen2g  8612  omxpen  8621  enen1  8659  enen2  8660  map2xp  8689  pwen  8692  ssenen  8693  phplem4  8701  php3  8705  snnen2o  8709  fineqvlem  8734  ssfi  8740  en1eqsn  8750  dif1en  8753  unfi  8787  unxpwdom2  9054  infdifsn  9122  infdiffi  9123  karden  9326  xpnum  9382  cardidm  9390  ficardom  9392  carden2a  9397  carden2b  9398  isinffi  9423  pm54.43  9431  pr2ne  9433  en2eqpr  9435  en2eleq  9436  infxpenlem  9441  infxpidm2  9445  mappwen  9540  finnisoeu  9541  djuen  9597  djuenun  9598  dju1dif  9600  djuassen  9606  mapdjuen  9608  pwdjuen  9609  infdju1  9617  pwdju1  9618  pwdjuidm  9619  cardadju  9622  ficardun  9626  pwsdompw  9628  infxp  9639  infmap2  9642  ackbij1lem5  9648  ackbij1lem9  9652  ackbij1b  9663  fin4en1  9733  isfin4p1  9739  fin23lem23  9750  domtriomlem  9866  axcclem  9881  carden  9975  alephadd  10001  gchdjuidm  10092  gchxpidm  10093  gchpwdom  10094  gchhar  10103  tskuni  10207  fzen2  13340  hashdvds  16114  unbenlem  16246  unben  16247  4sqlem11  16293  pmtrfconj  18596  psgnunilem1  18623  odinf  18692  dfod2  18693  sylow2blem1  18747  sylow2  18753  simpgnsgd  19224  frlmisfrlm  20994  hmphindis  22407  dyadmbl  24203  fnpreimac  30418  padct  30457  f1ocnt  30527  volmeas  31492  sconnpi1  32488  lzenom  39374  fiphp3d  39423  frlmpwfi  39705  isnumbasgrplem3  39712  fiuneneq  39804  rp-isfinite5  39890  enrelmap  40350  enrelmapr  40351  enmappw  40352  uspgrymrelen  44035