Theorem entr 8977

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

Syntax hints:   → wi 4   ∧ wa 395  ⊤wtru 1541  Vcvv 3447   class class class wbr 5107   Er wer 8668   ≈ cen 8915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-er 8671  df-en 8919

This theorem is referenced by:  entri  8979  snmapen1  9010  xpsnen2g  9034  omxpen  9043  enen1  9081  enen2  9082  map2xp  9111  pwen  9114  ssenen  9115  ssfiALT  9138  fineqvlem  9209  en1eqsnOLD  9220  dif1ennnALT  9222  unxpwdom2  9541  infdifsn  9610  infdiffi  9611  karden  9848  xpnum  9904  cardidm  9912  ficardom  9914  carden2a  9919  carden2b  9920  isinffi  9945  pm54.43  9954  pr2neOLD  9958  en2eqpr  9960  en2eleq  9961  infxpenlem  9966  infxpidm2  9970  mappwen  10065  finnisoeu  10066  djuen  10123  djuenun  10124  dju1dif  10126  djuassen  10132  mapdjuen  10134  pwdjuen  10135  infdju1  10143  pwdju1  10144  pwdjuidm  10145  cardadju  10148  nnadju  10151  ficardadju  10153  ficardun  10154  pwsdompw  10156  infxp  10167  infmap2  10170  ackbij1lem5  10176  ackbij1lem9  10180  ackbij1b  10191  fin4en1  10262  isfin4p1  10268  fin23lem23  10279  domtriomlem  10395  axcclem  10410  carden  10504  alephadd  10530  gchdjuidm  10621  gchxpidm  10622  gchpwdom  10623  gchhar  10632  tskuni  10736  fzen2  13934  hashdvds  16745  unbenlem  16879  unben  16880  4sqlem11  16926  pmtrfconj  19396  psgnunilem1  19423  odinf  19493  dfod2  19494  sylow2blem1  19550  sylow2  19556  simpgnsgd  20032  frlmisfrlm  21757  hmphindis  23684  dyadmbl  25501  fnpreimac  32595  padct  32643  f1ocnt  32725  volmeas  34221  sconnpi1  35226  lzenom  42758  fiphp3d  42807  frlmpwfi  43087  isnumbasgrplem3  43094  fiuneneq  43181  rp-isfinite5  43506  enrelmap  43986  enrelmapr  43987  enmappw  43988  uspgrymrelen  48141  termcterm2  49503