Metamath Proof Explorer


Theorem sneqi

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

Ref Expression
Hypothesis sneqi.1 A = B
Assertion sneqi A = B

Proof

Step Hyp Ref Expression
1 sneqi.1 A = B
2 sneq A = B A = B
3 1 2 ax-mp A = B