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

Theorem entr 6798
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 6794 . . . 4  |-  ~~  Er  _V
21a1i 12 . . 3  |-  (  T. 
->  ~~  Er  _V )
32ertr 6561 . 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 2727   class class class wbr 3920    Er wer 6543    ~~ cen 6746
This theorem is referenced by:  entri  6800  en2sn  6825  xpsnen2g  6840  omxpen  6849  enen1  6886  enen2  6887  map2xp  6916  pwen  6919  ssenen  6920  phplem4  6928  php3  6932  fineqvlem  6962  ssfi  6968  en1eqsn  6973  dif1enOLD  6975  dif1en  6976  unfi  7009  unxpwdom2  7186  infdifsn  7241  infdiffi  7242  karden  7449  xpnum  7468  cardidm  7476  ficardom  7478  carden2a  7483  carden2b  7484  isinffi  7509  pm54.43  7517  pr2ne  7519  en2eqpr  7521  infxpenlem  7525  infxpidm2  7528  mappwen  7623  finnisoeu  7624  cdaen  7683  cdaenun  7684  cda1dif  7686  cdaassen  7692  mapcdaen  7694  pwcdaen  7695  infcda1  7703  pwcdaidm  7705  cardacda  7708  ficardun  7712  pwsdompw  7714  infxp  7725  infmap2  7728  ackbij1lem5  7734  ackbij1lem9  7738  ackbij1b  7749  fin4en1  7819  isfin4-3  7825  fin23lem23  7836  domtriomlem  7952  axcclem  7967  carden  8055  alephadd  8079  gchcdaidm  8170  gchxpidm  8171  gchhar  8173  gchpwdom  8176  tskuni  8285  fzen2  10909  isprm2lem  12639  hashdvds  12717  unbenlem  12829  unben  12830  4sqlem11  12876  odinf  14711  dfod2  14712  sylow2blem1  14766  sylow2  14772  hmphindis  17320  dyadmbl  18787  sconpi1  22941  carinttar  25068  lzenom  26015  fiphp3d  26068  frlmpwfi  26428  isnumbasgrplem3  26436  en2eleq  26547  pmtrfconj  26573  psgnunilem1  26582  fiuneneq  26679
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fo 4606  df-f1o 4607  df-er 6546  df-en 6750
  Copyright terms: Public domain W3C validator