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

Proof

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