Theorem entr 9002

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

Syntax hints:   → wi 4   ∧ wa 397  ⊤wtru 1543  Vcvv 3475   class class class wbr 5149   Er wer 8700   ≈ cen 8936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-er 8703  df-en 8940

This theorem is referenced by:  entri  9004  snmapen1  9039  en2snOLDOLD  9043  xpsnen2g  9065  omxpen  9074  enen1  9117  enen2  9118  map2xp  9147  pwen  9150  ssenen  9151  ssfiALT  9174  phplem4OLD  9220  php3OLD  9224  snnen2oOLD  9227  fineqvlem  9262  en1eqsnOLD  9275  dif1ennnALT  9277  unfiOLD  9313  unxpwdom2  9583  infdifsn  9652  infdiffi  9653  karden  9890  xpnum  9946  cardidm  9954  ficardom  9956  carden2a  9961  carden2b  9962  isinffi  9987  pm54.43  9996  pr2neOLD  10000  en2eqpr  10002  en2eleq  10003  infxpenlem  10008  infxpidm2  10012  mappwen  10107  finnisoeu  10108  djuen  10164  djuenun  10165  dju1dif  10167  djuassen  10173  mapdjuen  10175  pwdjuen  10176  infdju1  10184  pwdju1  10185  pwdjuidm  10186  cardadju  10189  nnadju  10192  ficardadju  10194  ficardun  10195  ficardunOLD  10196  pwsdompw  10199  infxp  10210  infmap2  10213  ackbij1lem5  10219  ackbij1lem9  10223  ackbij1b  10234  fin4en1  10304  isfin4p1  10310  fin23lem23  10321  domtriomlem  10437  axcclem  10452  carden  10546  alephadd  10572  gchdjuidm  10663  gchxpidm  10664  gchpwdom  10665  gchhar  10674  tskuni  10778  fzen2  13934  hashdvds  16708  unbenlem  16841  unben  16842  4sqlem11  16888  pmtrfconj  19334  psgnunilem1  19361  odinf  19431  dfod2  19432  sylow2blem1  19488  sylow2  19494  simpgnsgd  19970  frlmisfrlm  21403  hmphindis  23301  dyadmbl  25117  fnpreimac  31896  padct  31944  f1ocnt  32013  volmeas  33229  sconnpi1  34230  lzenom  41508  fiphp3d  41557  frlmpwfi  41840  isnumbasgrplem3  41847  fiuneneq  41939  rp-isfinite5  42268  enrelmap  42748  enrelmapr  42749  enmappw  42750  uspgrymrelen  46531