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=BA=B

Proof

Step Hyp Ref Expression
1 eqeq2 A=Bx=Ax=B
2 1 abbidv A=Bx|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=BA=B