Theorem entr 8955

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1543  Vcvv 3430   class class class wbr 5086   Er wer 8642   ≈ cen 8892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pow 5308  ax-pr 5376  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-er 8645  df-en 8896

This theorem is referenced by:  entri  8957  snmapen1  8988  xpsnen2g  9010  omxpen  9019  enen1  9057  enen2  9058  map2xp  9087  pwen  9090  ssenen  9091  ssfiALT  9110  fineqvlem  9178  dif1ennnALT  9189  unxpwdom2  9505  infdifsn  9580  infdiffi  9581  karden  9821  xpnum  9877  cardidm  9885  ficardom  9887  carden2a  9892  carden2b  9893  isinffi  9918  pm54.43  9927  en2eqpr  9931  en2eleq  9932  infxpenlem  9937  infxpidm2  9941  mappwen  10036  finnisoeu  10037  djuen  10094  djuenun  10095  dju1dif  10097  djuassen  10103  mapdjuen  10105  pwdjuen  10106  infdju1  10114  pwdju1  10115  pwdjuidm  10116  cardadju  10119  nnadju  10122  ficardadju  10124  ficardun  10125  pwsdompw  10127  infxp  10138  infmap2  10141  ackbij1lem5  10147  ackbij1lem9  10151  ackbij1b  10162  fin4en1  10233  isfin4p1  10239  fin23lem23  10250  domtriomlem  10366  axcclem  10381  carden  10475  alephadd  10502  gchdjuidm  10593  gchxpidm  10594  gchpwdom  10595  gchhar  10604  tskuni  10708  fzen2  13933  hashdvds  16747  unbenlem  16881  unben  16882  4sqlem11  16928  pmtrfconj  19443  psgnunilem1  19470  odinf  19540  dfod2  19541  sylow2blem1  19597  sylow2  19603  simpgnsgd  20079  frlmisfrlm  21830  hmphindis  23764  dyadmbl  25569  fnpreimac  32745  padct  32793  f1ocnt  32875  volmeas  34377  sconnpi1  35423  lzenom  43204  fiphp3d  43249  frlmpwfi  43528  isnumbasgrplem3  43535  fiuneneq  43622  rp-isfinite5  43946  enrelmap  44426  enrelmapr  44427  enmappw  44428  uspgrymrelen  48631  termcterm2  49991