MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  entr Structured version   Visualization version   GIF version

Theorem entr 7993
Description: Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
Assertion
Ref Expression
entr ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

Proof of Theorem entr
StepHypRef Expression
1 ener 7987 . . . 4 ≈ Er V
21a1i 11 . . 3 (⊤ → ≈ Er V)
32ertr 7742 . 2 (⊤ → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
43trud 1491 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wtru 1482  Vcvv 3195   class class class wbr 4644   Er wer 7724  cen 7937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-er 7727  df-en 7941
This theorem is referenced by:  entri  7995  en2sn  8022  xpsnen2g  8038  omxpen  8047  enen1  8085  enen2  8086  map2xp  8115  pwen  8118  ssenen  8119  phplem4  8127  php3  8131  snnen2o  8134  fineqvlem  8159  ssfi  8165  en1eqsn  8175  dif1en  8178  unfi  8212  unxpwdom2  8478  infdifsn  8539  infdiffi  8540  karden  8743  xpnum  8762  cardidm  8770  ficardom  8772  carden2a  8777  carden2b  8778  isinffi  8803  pm54.43  8811  pr2ne  8813  en2eqpr  8815  en2eleq  8816  infxpenlem  8821  infxpidm2  8825  mappwen  8920  finnisoeu  8921  cdaen  8980  cdaenun  8981  cda1dif  8983  cdaassen  8989  mapcdaen  8991  pwcdaen  8992  infcda1  9000  pwcdaidm  9002  cardacda  9005  ficardun  9009  pwsdompw  9011  infxp  9022  infmap2  9025  ackbij1lem5  9031  ackbij1lem9  9035  ackbij1b  9046  fin4en1  9116  isfin4-3  9122  fin23lem23  9133  domtriomlem  9249  axcclem  9264  carden  9358  alephadd  9384  gchcdaidm  9475  gchxpidm  9476  gchpwdom  9477  gchhar  9486  tskuni  9590  fzen2  12751  isprm2lem  15375  hashdvds  15461  unbenlem  15593  unben  15594  4sqlem11  15640  pmtrfconj  17867  psgnunilem1  17894  odinf  17961  dfod2  17962  sylow2blem1  18016  sylow2  18022  frlmisfrlm  20168  hmphindis  21581  dyadmbl  23349  padct  29471  f1ocnt  29533  volmeas  30268  sconnpi1  31195  lzenom  37152  fiphp3d  37202  frlmpwfi  37487  isnumbasgrplem3  37494  fiuneneq  37594  rp-isfinite5  37682  enrelmap  38111  enrelmapr  38112  enmappw  38113  uspgrymrelen  41526
  Copyright terms: Public domain W3C validator