Theorem sneqi

Description: Equality inference for singletons. (Contributed by NM, 22-Jan-2004)

	Ref	Expression
Hypothesis	sneqi.1	$$⊢A=B$$
Assertion	sneqi	$$⊢\left\{A\right\}=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		sneqi.1	$$⊢A=B$$
2		sneq	$$⊢A=B\to \left\{A\right\}=\left\{B\right\}$$
3	1 2	ax-mp	$$⊢\left\{A\right\}=\left\{B\right\}$$