Theorem entr 8008

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

Syntax hints:   → wi 4   ∧ wa 384  ⊤wtru 1484  Vcvv 3200   class class class wbr 4653   Er wer 7739   ≈ cen 7952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-er 7742  df-en 7956

This theorem is referenced by:  entri  8010  en2sn  8037  xpsnen2g  8053  omxpen  8062  enen1  8100  enen2  8101  map2xp  8130  pwen  8133  ssenen  8134  phplem4  8142  php3  8146  snnen2o  8149  fineqvlem  8174  ssfi  8180  en1eqsn  8190  dif1en  8193  unfi  8227  unxpwdom2  8493  infdifsn  8554  infdiffi  8555  karden  8758  xpnum  8777  cardidm  8785  ficardom  8787  carden2a  8792  carden2b  8793  isinffi  8818  pm54.43  8826  pr2ne  8828  en2eqpr  8830  en2eleq  8831  infxpenlem  8836  infxpidm2  8840  mappwen  8935  finnisoeu  8936  cdaen  8995  cdaenun  8996  cda1dif  8998  cdaassen  9004  mapcdaen  9006  pwcdaen  9007  infcda1  9015  pwcdaidm  9017  cardacda  9020  ficardun  9024  pwsdompw  9026  infxp  9037  infmap2  9040  ackbij1lem5  9046  ackbij1lem9  9050  ackbij1b  9061  fin4en1  9131  isfin4-3  9137  fin23lem23  9148  domtriomlem  9264  axcclem  9279  carden  9373  alephadd  9399  gchcdaidm  9490  gchxpidm  9491  gchpwdom  9492  gchhar  9501  tskuni  9605  fzen2  12768  hashdvds  15480  unbenlem  15612  unben  15613  4sqlem11  15659  pmtrfconj  17886  psgnunilem1  17913  odinf  17980  dfod2  17981  sylow2blem1  18035  sylow2  18041  frlmisfrlm  20187  hmphindis  21600  dyadmbl  23368  padct  29497  f1ocnt  29559  volmeas  30294  sconnpi1  31221  lzenom  37333  fiphp3d  37383  frlmpwfi  37668  isnumbasgrplem3  37675  fiuneneq  37775  rp-isfinite5  37863  enrelmap  38291  enrelmapr  38292  enmappw  38293  uspgrymrelen  41761