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

Theorem entr 6908
Description: Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
Assertion
Ref Expression
entr  |-  ( ( A  ~~  B  /\  B  ~~  C )  ->  A  ~~  C )

Proof of Theorem entr
StepHypRef Expression
1 ener 6903 . . . 4  |-  ~~  Er  _V
21a1i 12 . . 3  |-  (  T. 
->  ~~  Er  _V )
32ertr 6670 . 2  |-  (  T. 
->  ( ( A  ~~  B  /\  B  ~~  C
)  ->  A  ~~  C ) )
43trud 1320 1  |-  ( ( A  ~~  B  /\  B  ~~  C )  ->  A  ~~  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    T. wtru 1312   _Vcvv 2789   class class class wbr 4024    Er wer 6652    ~~ cen 6855
This theorem is referenced by:  entri  6910  en2sn  6935  xpsnen2g  6950  omxpen  6959  enen1  6996  enen2  6997  map2xp  7026  pwen  7029  ssenen  7030  phplem4  7038  php3  7042  fineqvlem  7072  ssfi  7078  en1eqsn  7083  dif1enOLD  7085  dif1en  7086  unfi  7119  unxpwdom2  7297  infdifsn  7352  infdiffi  7353  karden  7560  xpnum  7579  cardidm  7587  ficardom  7589  carden2a  7594  carden2b  7595  isinffi  7620  pm54.43  7628  pr2ne  7630  en2eqpr  7632  infxpenlem  7636  infxpidm2  7639  mappwen  7734  finnisoeu  7735  cdaen  7794  cdaenun  7795  cda1dif  7797  cdaassen  7803  mapcdaen  7805  pwcdaen  7806  infcda1  7814  pwcdaidm  7816  cardacda  7819  ficardun  7823  pwsdompw  7825  infxp  7836  infmap2  7839  ackbij1lem5  7845  ackbij1lem9  7849  ackbij1b  7860  fin4en1  7930  isfin4-3  7936  fin23lem23  7947  domtriomlem  8063  axcclem  8078  carden  8168  alephadd  8194  gchcdaidm  8285  gchxpidm  8286  gchhar  8288  gchpwdom  8291  tskuni  8400  fzen2  11025  isprm2lem  12759  hashdvds  12837  unbenlem  12949  unben  12950  4sqlem11  12996  odinf  14870  dfod2  14871  sylow2blem1  14925  sylow2  14931  hmphindis  17482  dyadmbl  18949  sconpi1  23174  carinttar  25301  lzenom  26248  fiphp3d  26301  frlmpwfi  26661  isnumbasgrplem3  26669  en2eleq  26780  pmtrfconj  26806  psgnunilem1  26815  fiuneneq  26912
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-13 1690  ax-14 1692  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-er 6655  df-en 6859
  Copyright terms: Public domain W3C validator