Theorem eqs_refl ≪ | index | src | ≫

集合等号自反性

theorem eqs_refl (x: set): $ x = x $;

Step	Hyp	Ref	Expression
1		fo_imp_inslsto_ex_absrs	\fo y (y = x \imp x = x) \imp \ex y y = x \imp x = x
2		imp_imp_assiml	(y = x \imp y = x \imp x = x) \imp y = x \imp x = x
3		equality	y = x \imp y = x \imp x = x
4	2, 3	ax_mp	y = x \imp x = x
5	4	intro_fo	\fo y (y = x \imp x = x)
6	1, 5	ax_mp	\ex y y = x \imp x = x
7		existene	\ex y y = x
8	6, 7	ax_mp	x = x

Axiom use

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