Theorem entr 9012

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ⊤wtru 1571  Vcvv 3450   class class class wbr 5103   Er wer 8693   ≈ cen 8949

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-er 8696  df-en 8953

This theorem is used by:  entri  9014  snmapen1  9046  xpsnen2g  9068  omxpen  9077  enen1  9115  enen2  9116  map2xp  9145  pwen  9148  ssenen  9149  ssfiALT  9168  fineqvlem  9236  dif1ennnALT  9247  unxpwdom2  9560  infdifsn  9636  infdiffi  9637  karden  9898  kardenOLD  9899  xpnum  9956  cardidm  9964  ficardom  9966  carden2a  9971  carden2b  9972  isinffi  9997  pm54.43  10006  en2eqpr  10010  en2eleq  10011  infxpenlem  10016  infxpidm2  10020  mappwen  10115  finnisoeu  10116  djuen  10172  djuenun  10173  dju1dif  10175  djuassen  10181  mapdjuen  10183  pwdjuen  10184  infdju1  10192  pwdju1  10193  pwdjuidm  10194  cardadju  10197  nnadju  10200  ficardadju  10202  ficardun  10203  pwsdompw  10205  infxp  10216  infmap2  10219  ackbij1lem5  10225  ackbij1lem9  10229  ackbij1b  10240  fin4en1  10311  isfin4p1  10317  fin23lem23  10328  domtriomlem  10444  axcclem  10459  carden  10559  alephadd  10586  gchdjuidm  10677  gchxpidm  10678  gchpwdom  10679  gchhar  10688  tskuni  10792  fzen2  14033  hashdvds  16866  unbenlem  17000  unben  17001  4sqlem11  17047  pmtrfconj  19593  psgnunilem1  19620  odinf  19690  dfod2  19691  sylow2blem1  19747  sylow2  19753  simpgnsgd  20229  frlmisfrlm  22061  hmphindis  24023  dyadmbl  25828  fnpreimac  33143  padct  33189  f1ocnt  33271  volmeas  34742  kardexen  35689  sconnpi1  35818  lzenom  43615  fiphp3d  43660  frlmpwfi  43939  isnumbasgrplem3  43946  fiuneneq  44033  rp-isfinite5  44357  enrelmap  44837  enrelmapr  44838  enmappw  44839  uspgrymrelen  49069  termcterm2  50440