Theorem entr 9066

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1538  Vcvv 3488   class class class wbr 5166   Er wer 8760   ≈ cen 9000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-er 8763  df-en 9004

This theorem is referenced by:  entri  9068  snmapen1  9104  xpsnen2g  9131  omxpen  9140  enen1  9183  enen2  9184  map2xp  9213  pwen  9216  ssenen  9217  ssfiALT  9241  phplem4OLD  9283  php3OLD  9287  snnen2oOLD  9290  fineqvlem  9325  en1eqsnOLD  9337  dif1ennnALT  9339  unxpwdom2  9657  infdifsn  9726  infdiffi  9727  karden  9964  xpnum  10020  cardidm  10028  ficardom  10030  carden2a  10035  carden2b  10036  isinffi  10061  pm54.43  10070  pr2neOLD  10074  en2eqpr  10076  en2eleq  10077  infxpenlem  10082  infxpidm2  10086  mappwen  10181  finnisoeu  10182  djuen  10239  djuenun  10240  dju1dif  10242  djuassen  10248  mapdjuen  10250  pwdjuen  10251  infdju1  10259  pwdju1  10260  pwdjuidm  10261  cardadju  10264  nnadju  10267  ficardadju  10269  ficardun  10270  pwsdompw  10272  infxp  10283  infmap2  10286  ackbij1lem5  10292  ackbij1lem9  10296  ackbij1b  10307  fin4en1  10378  isfin4p1  10384  fin23lem23  10395  domtriomlem  10511  axcclem  10526  carden  10620  alephadd  10646  gchdjuidm  10737  gchxpidm  10738  gchpwdom  10739  gchhar  10748  tskuni  10852  fzen2  14020  hashdvds  16822  unbenlem  16955  unben  16956  4sqlem11  17002  pmtrfconj  19508  psgnunilem1  19535  odinf  19605  dfod2  19606  sylow2blem1  19662  sylow2  19668  simpgnsgd  20144  frlmisfrlm  21891  hmphindis  23826  dyadmbl  25654  fnpreimac  32689  padct  32733  f1ocnt  32807  volmeas  34195  sconnpi1  35207  lzenom  42726  fiphp3d  42775  frlmpwfi  43055  isnumbasgrplem3  43062  fiuneneq  43153  rp-isfinite5  43479  enrelmap  43959  enrelmapr  43960  enmappw  43961  uspgrymrelen  47876