Theorem entr 4475

Description: Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.

Assertion

Ref	Expression
entr	|- ((A ~~ B /\ B ~~ C) -> A ~~ C)

Proof of Theorem entr

Step	Hyp	Ref	Expression
1		relen 4433	. 2 |- Rel ~~
2		visset 1860	. . 3 |- x e. V
3		visset 1860	. . 3 |- y e. V
4		visset 1860	. . 3 |- z e. V
5		ener 4471	. . 3 |- Er ~~
6	2, 3, 4, 5	ertr 4332	. 2 |- ((x ~~ y /\ y ~~ z) -> x ~~ z)
7	2	enref 4452	. 2 |- x ~~ x
8	1, 6, 7	vtoclrbr 3269	1 |- ((A ~~ B /\ B ~~ C) -> A ~~ C)

Syntax hints:   -> wi 3   /\ wa 230   class class class wbr 2674   ~~ cen 4425

This theorem is referenced by:  entri 4477  en2sn 4492  sdomdomtr 4532  ensdomtr 4534  domsdomtr 4539  enen1 4540  enen2 4541  xpen 4553  ssenen 4569  phplem4 4576  php3 4580  isfinite1 4595  ssfi 4601  unfi 4614  pm54.43 4632  karden 4788  oncard 4892  carden 4894  unbenlem 7596  unben 7597  infxpidmlem1 7644  infxpidmlem12 7655  infcda 7659  infxp 7664  infmap2 7673  alephadd 7674  set2elt 10639  setwoe 10640  top2usne 10643  homindlem2 10644  homindlem3 10645

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-pow 2798  ax-pr 2835  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-rex 1697  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-id 2891  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-f1 3252  df-fo 3253  df-f1o 3254  df-er 4319  df-en 4429

Copyright terms: Public domain