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

Theorem entr 8549
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 8544 . . . 4 ≈ Er V
21a1i 11 . . 3 (⊤ → ≈ Er V)
32ertr 8293 . 2 (⊤ → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
43mptru 1535 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wtru 1529  Vcvv 3492   class class class wbr 5057   Er wer 8275  cen 8494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-er 8278  df-en 8498
This theorem is referenced by:  entri  8551  snmapen1  8579  en2sn  8581  xpsnen2g  8598  omxpen  8607  enen1  8645  enen2  8646  map2xp  8675  pwen  8678  ssenen  8679  phplem4  8687  php3  8691  snnen2o  8695  fineqvlem  8720  ssfi  8726  en1eqsn  8736  dif1en  8739  unfi  8773  unxpwdom2  9040  infdifsn  9108  infdiffi  9109  karden  9312  xpnum  9368  cardidm  9376  ficardom  9378  carden2a  9383  carden2b  9384  isinffi  9409  pm54.43  9417  pr2ne  9419  en2eqpr  9421  en2eleq  9422  infxpenlem  9427  infxpidm2  9431  mappwen  9526  finnisoeu  9527  djuen  9583  djuenun  9584  dju1dif  9586  djuassen  9592  mapdjuen  9594  pwdjuen  9595  infdju1  9603  pwdju1  9604  pwdjuidm  9605  cardadju  9608  ficardun  9612  pwsdompw  9614  infxp  9625  infmap2  9628  ackbij1lem5  9634  ackbij1lem9  9638  ackbij1b  9649  fin4en1  9719  isfin4p1  9725  fin23lem23  9736  domtriomlem  9852  axcclem  9867  carden  9961  alephadd  9987  gchdjuidm  10078  gchxpidm  10079  gchpwdom  10080  gchhar  10089  tskuni  10193  fzen2  13325  hashdvds  16100  unbenlem  16232  unben  16233  4sqlem11  16279  pmtrfconj  18523  psgnunilem1  18550  odinf  18619  dfod2  18620  sylow2blem1  18674  sylow2  18680  simpgnsgd  19151  frlmisfrlm  20920  hmphindis  22333  dyadmbl  24128  fnpreimac  30344  padct  30381  f1ocnt  30451  volmeas  31389  sconnpi1  32383  lzenom  39245  fiphp3d  39294  frlmpwfi  39576  isnumbasgrplem3  39583  fiuneneq  39675  rp-isfinite5  39761  enrelmap  40221  enrelmapr  40222  enmappw  40223  uspgrymrelen  43905
  Copyright terms: Public domain W3C validator