Theorem eqs_tran ≪ | index | src | ≫

集合等号传递性

theorem eqs_tran (x y z: set): $ x = y \imp y = z \imp x = z $;

Step	Hyp	Ref	Expression
1		imp_tran	(x = y \imp y = x) \imp (y = x \imp y = z \imp x = z) \imp x = y \imp y = z \imp x = z
2		eqs_sym	x = y \imp y = x
3	1, 2	ax_mp	(y = x \imp y = z \imp x = z) \imp x = y \imp y = z \imp x = z
4		equality	y = x \imp y = z \imp x = z
5	3, 4	ax_mp	x = y \imp y = z \imp x = z

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7)