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

Theorem entr 7001
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 6996 . . . 4  |-  ~~  Er  _V
21a1i 10 . . 3  |-  (  T. 
->  ~~  Er  _V )
32ertr 6762 . 2  |-  (  T. 
->  ( ( A  ~~  B  /\  B  ~~  C
)  ->  A  ~~  C ) )
43trud 1323 1  |-  ( ( A  ~~  B  /\  B  ~~  C )  ->  A  ~~  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    T. wtru 1316   _Vcvv 2864   class class class wbr 4104    Er wer 6744    ~~ cen 6948
This theorem is referenced by:  entri  7003  en2sn  7028  xpsnen2g  7043  omxpen  7052  enen1  7089  enen2  7090  map2xp  7119  pwen  7122  ssenen  7123  phplem4  7131  php3  7135  fineqvlem  7165  ssfi  7171  en1eqsn  7178  dif1enOLD  7180  dif1en  7181  unfi  7214  unxpwdom2  7392  infdifsn  7447  infdiffi  7448  karden  7655  xpnum  7674  cardidm  7682  ficardom  7684  carden2a  7689  carden2b  7690  isinffi  7715  pm54.43  7723  pr2ne  7725  en2eqpr  7727  infxpenlem  7731  infxpidm2  7734  mappwen  7829  finnisoeu  7830  cdaen  7889  cdaenun  7890  cda1dif  7892  cdaassen  7898  mapcdaen  7900  pwcdaen  7901  infcda1  7909  pwcdaidm  7911  cardacda  7914  ficardun  7918  pwsdompw  7920  infxp  7931  infmap2  7934  ackbij1lem5  7940  ackbij1lem9  7944  ackbij1b  7955  fin4en1  8025  isfin4-3  8031  fin23lem23  8042  domtriomlem  8158  axcclem  8173  carden  8263  alephadd  8289  gchcdaidm  8380  gchxpidm  8381  gchhar  8383  gchpwdom  8386  tskuni  8495  fzen2  11123  isprm2lem  12862  hashdvds  12940  unbenlem  13052  unben  13053  4sqlem11  13099  odinf  14975  dfod2  14976  sylow2blem1  15030  sylow2  15036  hmphindis  17594  dyadmbl  19059  volmeas  23851  sconpi1  24174  lzenom  26172  fiphp3d  26225  frlmpwfi  26585  isnumbasgrplem3  26593  en2eleq  26704  pmtrfconj  26730  psgnunilem1  26739  fiuneneq  26836  hashf1rn  27494
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-er 6747  df-en 6952
  Copyright terms: Public domain W3C validator