Theorem entr 8724

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

Syntax hints:   → wi 4   ∧ wa 399  ⊤wtru 1544  Vcvv 3423   class class class wbr 5070   Er wer 8430   ≈ cen 8665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5479  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-er 8433  df-en 8669

This theorem is referenced by:  entri  8726  snmapen1  8760  en2snOLDOLD  8764  xpsnen2g  8782  omxpen  8791  enen1  8830  enen2  8831  map2xp  8860  pwen  8863  ssenen  8864  phplem4  8872  php3  8876  snnen2o  8880  ssfiALT  8896  fineqvlem  8940  en1eqsn  8952  dif1enALT  8955  unfiOLD  8986  unxpwdom2  9252  infdifsn  9320  infdiffi  9321  karden  9559  xpnum  9615  cardidm  9623  ficardom  9625  carden2a  9630  carden2b  9631  isinffi  9656  pm54.43  9665  pr2ne  9667  en2eqpr  9669  en2eleq  9670  infxpenlem  9675  infxpidm2  9679  mappwen  9774  finnisoeu  9775  djuen  9831  djuenun  9832  dju1dif  9834  djuassen  9840  mapdjuen  9842  pwdjuen  9843  infdju1  9851  pwdju1  9852  pwdjuidm  9853  cardadju  9856  nnadju  9859  ficardadju  9861  ficardun  9862  ficardunOLD  9863  pwsdompw  9866  infxp  9877  infmap2  9880  ackbij1lem5  9886  ackbij1lem9  9890  ackbij1b  9901  fin4en1  9971  isfin4p1  9977  fin23lem23  9988  domtriomlem  10104  axcclem  10119  carden  10213  alephadd  10239  gchdjuidm  10330  gchxpidm  10331  gchpwdom  10332  gchhar  10341  tskuni  10445  fzen2  13592  hashdvds  16379  unbenlem  16512  unben  16513  4sqlem11  16559  pmtrfconj  18964  psgnunilem1  18991  odinf  19060  dfod2  19061  sylow2blem1  19115  sylow2  19121  simpgnsgd  19593  frlmisfrlm  20940  hmphindis  22831  dyadmbl  24644  fnpreimac  30885  padct  30931  f1ocnt  31000  volmeas  32074  sconnpi1  33076  lzenom  40480  fiphp3d  40529  frlmpwfi  40811  isnumbasgrplem3  40818  fiuneneq  40910  rp-isfinite5  40994  enrelmap  41467  enrelmapr  41468  enmappw  41469  uspgrymrelen  45176