Metamath Proof Explorer


Theorem sneqd

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

Ref Expression
Hypothesis sneqd.1 φA=B
Assertion sneqd φA=B

Proof

Step Hyp Ref Expression
1 sneqd.1 φA=B
2 sneq A=BA=B
3 1 2 syl φA=B