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

Theorem entr 7569
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 7564 . . . 4  |-  ~~  Er  _V
21a1i 11 . . 3  |-  ( T. 
->  ~~  Er  _V )
32ertr 7328 . 2  |-  ( T. 
->  ( ( A  ~~  B  /\  B  ~~  C
)  ->  A  ~~  C ) )
43trud 1392 1  |-  ( ( A  ~~  B  /\  B  ~~  C )  ->  A  ~~  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   T. wtru 1384   _Vcvv 3095   class class class wbr 4437    Er wer 7310    ~~ cen 7515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-er 7313  df-en 7519
This theorem is referenced by:  entri  7571  en2sn  7597  xpsnen2g  7612  omxpen  7621  enen1  7659  enen2  7660  map2xp  7689  pwen  7692  ssenen  7693  phplem4  7701  php3  7705  snnen2o  7708  fineqvlem  7736  ssfi  7742  en1eqsn  7751  dif1enOLD  7754  dif1en  7755  unfi  7789  unxpwdom2  8017  infdifsn  8076  infdiffi  8077  karden  8316  xpnum  8335  cardidm  8343  ficardom  8345  carden2a  8350  carden2b  8351  isinffi  8376  pm54.43  8384  pr2ne  8386  en2eqpr  8388  en2eleq  8389  infxpenlem  8394  infxpidm2  8397  mappwen  8496  finnisoeu  8497  cdaen  8556  cdaenun  8557  cda1dif  8559  cdaassen  8565  mapcdaen  8567  pwcdaen  8568  infcda1  8576  pwcdaidm  8578  cardacda  8581  ficardun  8585  pwsdompw  8587  infxp  8598  infmap2  8601  ackbij1lem5  8607  ackbij1lem9  8611  ackbij1b  8622  fin4en1  8692  isfin4-3  8698  fin23lem23  8709  domtriomlem  8825  axcclem  8840  carden  8929  alephadd  8955  gchcdaidm  9049  gchxpidm  9050  gchpwdom  9051  gchhar  9060  tskuni  9164  fzen2  12061  isprm2lem  14206  hashdvds  14287  unbenlem  14408  unben  14409  4sqlem11  14455  pmtrfconj  16470  psgnunilem1  16497  odinf  16564  dfod2  16565  sylow2blem1  16619  sylow2  16625  frlmisfrlm  18861  hmphindis  20276  dyadmbl  21987  volmeas  28181  sconpi1  28662  lzenom  30679  fiphp3d  30729  frlmpwfi  31022  isnumbasgrplem3  31030  fiuneneq  31130  rp-isfinite5  37581
  Copyright terms: Public domain W3C validator