ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  entr Unicode version

Theorem entr 6780
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 6775 . . . 4  |-  ~~  Er  _V
21a1i 9 . . 3  |-  ( T. 
->  ~~  Er  _V )
32ertr 6546 . 2  |-  ( T. 
->  ( ( A  ~~  B  /\  B  ~~  C
)  ->  A  ~~  C ) )
43mptru 1362 1  |-  ( ( A  ~~  B  /\  B  ~~  C )  ->  A  ~~  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104   T. wtru 1354   _Vcvv 2737   class class class wbr 4002    Er wer 6528    ~~ cen 6734
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4120  ax-pow 4173  ax-pr 4208  ax-un 4432
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4003  df-opab 4064  df-id 4292  df-xp 4631  df-rel 4632  df-cnv 4633  df-co 4634  df-dm 4635  df-rn 4636  df-res 4637  df-ima 4638  df-fun 5216  df-fn 5217  df-f 5218  df-f1 5219  df-fo 5220  df-f1o 5221  df-er 6531  df-en 6737
This theorem is referenced by:  entri  6782  en2sn  6809  xpsnen2g  6825  enen1  6836  enen2  6837  ssenen  6847  phplem4  6851  snnen2og  6855  php5dom  6859  phplem4on  6863  dif1en  6875  dif1enen  6876  fisbth  6879  diffisn  6889  unsnfidcex  6915  unsnfidcel  6916  f1finf1o  6942  en1eqsn  6943  endjusym  7091  carden2bex  7184  pm54.43  7185  pr2ne  7187  djuen  7206  djuenun  7207  djuassen  7212  frecfzen2  10421  uzennn  10430  hashunlem  10776  hashxp  10798  1nprm  12105  hashdvds  12212  unennn  12389  ennnfonelemen  12413  ennnfonelemim  12416  exmidunben  12418  ctinfom  12420  ctinf  12422  pwf1oexmid  14600
  Copyright terms: Public domain W3C validator