Theorem entr 9004

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

Syntax hints:   → wi 4   ∧ wa 400  ⊤wtru 1571  Vcvv 3455   class class class wbr 5110   Er wer 8692   ≈ cen 8941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-er 8695  df-en 8945

This theorem is referenced by:  entri  9006  snmapen1  9037  xpsnen2g  9059  omxpen  9068  enen1  9106  enen2  9107  map2xp  9136  pwen  9139  ssenen  9140  ssfiALT  9159  fineqvlem  9227  dif1ennnALT  9238  unxpwdom2  9551  infdifsn  9627  infdiffi  9628  karden  9882  xpnum  9938  cardidm  9946  ficardom  9948  carden2a  9953  carden2b  9954  isinffi  9979  pm54.43  9988  en2eqpr  9992  en2eleq  9993  infxpenlem  9998  infxpidm2  10002  mappwen  10097  finnisoeu  10098  djuen  10154  djuenun  10155  dju1dif  10157  djuassen  10163  mapdjuen  10165  pwdjuen  10166  infdju1  10174  pwdju1  10175  pwdjuidm  10176  cardadju  10179  nnadju  10182  ficardadju  10184  ficardun  10185  pwsdompw  10187  infxp  10198  infmap2  10201  ackbij1lem5  10207  ackbij1lem9  10211  ackbij1b  10222  fin4en1  10294  isfin4p1  10300  fin23lem23  10311  domtriomlem  10427  axcclem  10442  carden  10536  alephadd  10563  gchdjuidm  10654  gchxpidm  10655  gchpwdom  10656  gchhar  10665  tskuni  10769  fzen2  14007  hashdvds  16835  unbenlem  16969  unben  16970  4sqlem11  17016  pmtrfconj  19537  psgnunilem1  19564  odinf  19634  dfod2  19635  sylow2blem1  19691  sylow2  19697  simpgnsgd  20173  frlmisfrlm  21979  hmphindis  23935  dyadmbl  25740  fnpreimac  32996  padct  33044  f1ocnt  33126  volmeas  34602  kardexen  35557  sconnpi1  35712  lzenom  43484  fiphp3d  43529  frlmpwfi  43808  isnumbasgrplem3  43815  fiuneneq  43902  rp-isfinite5  44226  enrelmap  44706  enrelmapr  44707  enmappw  44708  uspgrymrelen  48901  termcterm2  50275