Theorem entr 8295

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

Syntax hints:   → wi 4   ∧ wa 386  ⊤wtru 1602  Vcvv 3398   class class class wbr 4888   Er wer 8025   ≈ cen 8240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-er 8028  df-en 8244

This theorem is referenced by:  entri  8297  snmapen1  8325  en2sn  8327  xpsnen2g  8343  omxpen  8352  enen1  8390  enen2  8391  map2xp  8420  pwen  8423  ssenen  8424  phplem4  8432  php3  8436  snnen2o  8439  fineqvlem  8464  ssfi  8470  en1eqsn  8480  dif1en  8483  unfi  8517  unxpwdom2  8784  infdifsn  8853  infdiffi  8854  karden  9057  xpnum  9112  cardidm  9120  ficardom  9122  carden2a  9127  carden2b  9128  isinffi  9153  pm54.43  9161  pr2ne  9163  en2eqpr  9165  en2eleq  9166  infxpenlem  9171  infxpidm2  9175  mappwen  9270  finnisoeu  9271  cdaen  9332  cdaenun  9333  cda1dif  9335  cdaassen  9341  mapcdaen  9343  pwcdaen  9344  infcda1  9352  pwcdaidm  9354  cardacda  9357  ficardun  9361  pwsdompw  9363  infxp  9374  infmap2  9377  ackbij1lem5  9383  ackbij1lem9  9387  ackbij1b  9398  fin4en1  9468  isfin4-3  9474  fin23lem23  9485  domtriomlem  9601  axcclem  9616  carden  9710  alephadd  9736  gchcdaidm  9827  gchxpidm  9828  gchpwdom  9829  gchhar  9838  tskuni  9942  fzen2  13091  hashdvds  15888  unbenlem  16020  unben  16021  4sqlem11  16067  pmtrfconj  18273  psgnunilem1  18300  odinf  18368  dfod2  18369  sylow2blem1  18423  sylow2  18429  frlmisfrlm  20595  hmphindis  22013  dyadmbl  23808  fnpreimac  30040  padct  30067  f1ocnt  30127  volmeas  30896  sconnpi1  31824  lzenom  38303  fiphp3d  38353  frlmpwfi  38637  isnumbasgrplem3  38644  fiuneneq  38744  rp-isfinite5  38830  enrelmap  39257  enrelmapr  39258  enmappw  39259  uspgrymrelen  42786