Theorem eqs_repl ≪ | index | src | ≫

集合等号左替换性

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

Step	Hyp	Ref	Expression
1		iff_comp	(x = z \imp y = z) \imp (y = z \imp x = z) \imp (x = z \iff y = z)
2	1	_hyp_null_complete	x = y \imp (x = z \imp y = z) \imp (y = z \imp x = z) \imp (x = z \iff y = z)
3		equality	x = y \imp x = z \imp y = z
4	3	_hyp_null_complete	x = y \imp x = y \imp x = z \imp y = z
5		_hyp_null_intro	x = y \imp x = y
6	4, 5	_hyp_mp	x = y \imp x = z \imp y = z
7	2, 6	_hyp_mp	x = y \imp (y = z \imp x = z) \imp (x = z \iff y = z)
8		eqs_tran	x = y \imp y = z \imp x = z
9	8	_hyp_null_complete	x = y \imp x = y \imp y = z \imp x = z
10	9, 5	_hyp_mp	x = y \imp y = z \imp x = z
11	7, 10	_hyp_mp	x = y \imp (x = z \iff y = z)

Axiom use

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