Theorem entr 8171

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 8166	. . . 4 ⊢ ≈ Er V
2	1	a1i 11	. . 3 ⊢ (⊤ → ≈ Er V)
3	2	ertr 7924	. 2 ⊢ (⊤ → ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶))
4	3	trud 1640	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 383  ⊤wtru 1631  Vcvv 3338   class class class wbr 4802   Er wer 7906   ≈ cen 8116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-id 5172  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-er 7909  df-en 8120

This theorem is referenced by:  entri  8173  en2sn  8200  xpsnen2g  8216  omxpen  8225  enen1  8263  enen2  8264  map2xp  8293  pwen  8296  ssenen  8297  phplem4  8305  php3  8309  snnen2o  8312  fineqvlem  8337  ssfi  8343  en1eqsn  8353  dif1en  8356  unfi  8390  unxpwdom2  8656  infdifsn  8725  infdiffi  8726  karden  8929  xpnum  8965  cardidm  8973  ficardom  8975  carden2a  8980  carden2b  8981  isinffi  9006  pm54.43  9014  pr2ne  9016  en2eqpr  9018  en2eleq  9019  infxpenlem  9024  infxpidm2  9028  mappwen  9123  finnisoeu  9124  cdaen  9185  cdaenun  9186  cda1dif  9188  cdaassen  9194  mapcdaen  9196  pwcdaen  9197  infcda1  9205  pwcdaidm  9207  cardacda  9210  ficardun  9214  pwsdompw  9216  infxp  9227  infmap2  9230  ackbij1lem5  9236  ackbij1lem9  9240  ackbij1b  9251  fin4en1  9321  isfin4-3  9327  fin23lem23  9338  domtriomlem  9454  axcclem  9469  carden  9563  alephadd  9589  gchcdaidm  9680  gchxpidm  9681  gchpwdom  9682  gchhar  9691  tskuni  9795  fzen2  12960  hashdvds  15680  unbenlem  15812  unben  15813  4sqlem11  15859  pmtrfconj  18084  psgnunilem1  18111  odinf  18178  dfod2  18179  sylow2blem1  18233  sylow2  18239  frlmisfrlm  20387  hmphindis  21800  dyadmbl  23566  padct  29804  f1ocnt  29866  volmeas  30601  sconnpi1  31526  lzenom  37833  fiphp3d  37883  frlmpwfi  38168  isnumbasgrplem3  38175  fiuneneq  38275  rp-isfinite5  38363  enrelmap  38791  enrelmapr  38792  enmappw  38793  uspgrymrelen  42269