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

Theorem entr 7587
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 7582 . . . 4
21a1i 11 . . 3
32ertr 7345 . 2
43trud 1404 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369   wtru 1396   cvv 3109   class class class wbr 4452  Erwer 7327   cen 7533
This theorem is referenced by:  entri  7589  en2sn  7615  xpsnen2g  7630  omxpen  7639  enen1  7677  enen2  7678  map2xp  7707  pwen  7710  ssenen  7711  phplem4  7719  php3  7723  snnen2o  7726  fineqvlem  7754  ssfi  7760  en1eqsn  7769  dif1enOLD  7772  dif1en  7773  unfi  7807  unxpwdom2  8035  infdifsn  8094  infdiffi  8095  karden  8334  xpnum  8353  cardidm  8361  ficardom  8363  carden2a  8368  carden2b  8369  isinffi  8394  pm54.43  8402  pr2ne  8404  en2eqpr  8406  en2eleq  8407  infxpenlem  8412  infxpidm2  8415  mappwen  8514  finnisoeu  8515  cdaen  8574  cdaenun  8575  cda1dif  8577  cdaassen  8583  mapcdaen  8585  pwcdaen  8586  infcda1  8594  pwcdaidm  8596  cardacda  8599  ficardun  8603  pwsdompw  8605  infxp  8616  infmap2  8619  ackbij1lem5  8625  ackbij1lem9  8629  ackbij1b  8640  fin4en1  8710  isfin4-3  8716  fin23lem23  8727  domtriomlem  8843  axcclem  8858  carden  8947  alephadd  8973  gchcdaidm  9067  gchxpidm  9068  gchpwdom  9069  gchhar  9078  tskuni  9182  fzen2  12079  isprm2lem  14224  hashdvds  14305  unbenlem  14426  unben  14427  4sqlem11  14473  pmtrfconj  16491  psgnunilem1  16518  odinf  16585  dfod2  16586  sylow2blem1  16640  sylow2  16646  frlmisfrlm  18883  hmphindis  20298  dyadmbl  22009  volmeas  28203  sconpi1  28684  lzenom  30703  fiphp3d  30753  frlmpwfi  31046  isnumbasgrplem3  31054  fiuneneq  31154  rp-isfinite5  37743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-er 7330  df-en 7537
  Copyright terms: Public domain W3C validator