Theorem entr 9045

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1538  Vcvv 3478   class class class wbr 5148   Er wer 8741   ≈ cen 8981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-er 8744  df-en 8985

This theorem is referenced by:  entri  9047  snmapen1  9078  xpsnen2g  9104  omxpen  9113  enen1  9156  enen2  9157  map2xp  9186  pwen  9189  ssenen  9190  ssfiALT  9213  phplem4OLD  9255  php3OLD  9259  snnen2oOLD  9262  fineqvlem  9296  en1eqsnOLD  9307  dif1ennnALT  9309  unxpwdom2  9626  infdifsn  9695  infdiffi  9696  karden  9933  xpnum  9989  cardidm  9997  ficardom  9999  carden2a  10004  carden2b  10005  isinffi  10030  pm54.43  10039  pr2neOLD  10043  en2eqpr  10045  en2eleq  10046  infxpenlem  10051  infxpidm2  10055  mappwen  10150  finnisoeu  10151  djuen  10208  djuenun  10209  dju1dif  10211  djuassen  10217  mapdjuen  10219  pwdjuen  10220  infdju1  10228  pwdju1  10229  pwdjuidm  10230  cardadju  10233  nnadju  10236  ficardadju  10238  ficardun  10239  pwsdompw  10241  infxp  10252  infmap2  10255  ackbij1lem5  10261  ackbij1lem9  10265  ackbij1b  10276  fin4en1  10347  isfin4p1  10353  fin23lem23  10364  domtriomlem  10480  axcclem  10495  carden  10589  alephadd  10615  gchdjuidm  10706  gchxpidm  10707  gchpwdom  10708  gchhar  10717  tskuni  10821  fzen2  14007  hashdvds  16809  unbenlem  16942  unben  16943  4sqlem11  16989  pmtrfconj  19499  psgnunilem1  19526  odinf  19596  dfod2  19597  sylow2blem1  19653  sylow2  19659  simpgnsgd  20135  frlmisfrlm  21886  hmphindis  23821  dyadmbl  25649  fnpreimac  32688  padct  32737  f1ocnt  32810  volmeas  34212  sconnpi1  35224  lzenom  42758  fiphp3d  42807  frlmpwfi  43087  isnumbasgrplem3  43094  fiuneneq  43181  rp-isfinite5  43507  enrelmap  43987  enrelmapr  43988  enmappw  43989  uspgrymrelen  47997