Theorem eqs_sym ≪ | index | src | ≫

集合等号对称性

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

Step	Hyp	Ref	Expression
1		imp_imp_elimrsl	(x = y \imp x = x \imp y = x) \imp x = x \imp x = y \imp y = x
2		equality	x = y \imp x = x \imp y = x
3	1, 2	ax_mp	x = x \imp x = y \imp y = x
4		eqs_refl	x = x
5	3, 4	ax_mp	x = y \imp y = x

Axiom use

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