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 \left\{A\right\}=\left\{B\right\}$$

Proof

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