Theorem eqs_repr ≪ | index | src | ≫

集合等号右替换性

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

Step	Hyp	Ref	Expression
1		iff_comp	(z = x \imp z = y) \imp (z = y \imp z = x) \imp (z = x \iff z = y)
2	1	_hyp_null_complete	x = y \imp (z = x \imp z = y) \imp (z = y \imp z = x) \imp (z = x \iff z = y)
3		imp_imp_swapl	(z = x \imp x = y \imp z = y) \imp x = y \imp z = x \imp z = y
4		eqs_tran	z = x \imp x = y \imp z = y
5	3, 4	ax_mp	x = y \imp z = x \imp z = y
6	5	_hyp_null_complete	x = y \imp x = y \imp z = x \imp z = y
7		_hyp_null_intro	x = y \imp x = y
8	6, 7	_hyp_mp	x = y \imp z = x \imp z = y
9	2, 8	_hyp_mp	x = y \imp (z = y \imp z = x) \imp (z = x \iff z = y)
10		imp_tran	(x = y \imp y = x) \imp (y = x \imp z = y \imp z = x) \imp x = y \imp z = y \imp z = x
11		eqs_sym	x = y \imp y = x
12	10, 11	ax_mp	(y = x \imp z = y \imp z = x) \imp x = y \imp z = y \imp z = x
13		imp_imp_swapl	(z = y \imp y = x \imp z = x) \imp y = x \imp z = y \imp z = x
14		eqs_tran	z = y \imp y = x \imp z = x
15	13, 14	ax_mp	y = x \imp z = y \imp z = x
16	12, 15	ax_mp	x = y \imp z = y \imp z = x
17	16	_hyp_null_complete	x = y \imp x = y \imp z = y \imp z = x
18	17, 7	_hyp_mp	x = y \imp z = y \imp z = x
19	9, 18	_hyp_mp	x = y \imp (z = x \iff z = y)

Axiom use

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