Theorem entr 8950

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

Syntax hints:   → wi 4   ∧ wa 396  ⊤wtru 1548  Vcvv 3432   class class class wbr 5079   Er wer 8637   ≈ cen 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-er 8640  df-en 8891

This theorem is referenced by:  entri  8952  snmapen1  8983  xpsnen2g  9005  omxpen  9014  enen1  9052  enen2  9053  map2xp  9082  pwen  9085  ssenen  9086  ssfiALT  9105  fineqvlem  9173  dif1ennnALT  9184  unxpwdom2  9500  infdifsn  9576  infdiffi  9577  karden  9817  xpnum  9873  cardidm  9881  ficardom  9883  carden2a  9888  carden2b  9889  isinffi  9914  pm54.43  9923  en2eqpr  9927  en2eleq  9928  infxpenlem  9933  infxpidm2  9937  mappwen  10032  finnisoeu  10033  djuen  10090  djuenun  10091  dju1dif  10093  djuassen  10099  mapdjuen  10101  pwdjuen  10102  infdju1  10110  pwdju1  10111  pwdjuidm  10112  cardadju  10115  nnadju  10118  ficardadju  10120  ficardun  10121  pwsdompw  10123  infxp  10134  infmap2  10137  ackbij1lem5  10143  ackbij1lem9  10147  ackbij1b  10158  fin4en1  10229  isfin4p1  10235  fin23lem23  10246  domtriomlem  10362  axcclem  10377  carden  10471  alephadd  10498  gchdjuidm  10589  gchxpidm  10590  gchpwdom  10591  gchhar  10600  tskuni  10704  fzen2  13929  hashdvds  16743  unbenlem  16877  unben  16878  4sqlem11  16924  pmtrfconj  19439  psgnunilem1  19466  odinf  19536  dfod2  19537  sylow2blem1  19593  sylow2  19599  simpgnsgd  20075  frlmisfrlm  21830  hmphindis  23787  dyadmbl  25592  fnpreimac  32769  padct  32817  f1ocnt  32899  volmeas  34422  sconnpi1  35474  lzenom  43226  fiphp3d  43271  frlmpwfi  43550  isnumbasgrplem3  43557  fiuneneq  43644  rp-isfinite5  43968  enrelmap  44448  enrelmapr  44449  enmappw  44450  uspgrymrelen  48651  termcterm2  50011