This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sneq

Description: Equality theorem for singletons. Part of Exercise 4 of TakeutiZaring p. 15. (Contributed by NM, 21-Jun-1993)

		Ref	Expression
	Assertion	sneq	$⊢ A = B \to \{A\} = \{B\}$

Step	Hyp	Ref	Expression
1		eqeq2	$⊢ A = B \to (x = A \leftrightarrow x = B)$
2	1	abbidv	$⊢ A = B \to \{x \| x = A\} = \{x \| x = B\}$
3		df-sn	$⊢ \{A\} = \{x \| x = A\}$
4		df-sn	$⊢ \{B\} = \{x \| x = B\}$
5	2 3 4	3eqtr4g	$⊢ A = B \to \{A\} = \{B\}$