Metamath Proof Explorer


Theorem eqsn

Description: Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007) (Proof shortened by JJ, 23-Jul-2021)

Ref Expression
Assertion eqsn A A = B x A x = B

Proof

Step Hyp Ref Expression
1 df-ne A ¬ A =
2 biorf ¬ A = A = B A = A = B
3 1 2 sylbi A A = B A = A = B
4 dfss3 A B x A x B
5 sssn A B A = A = B
6 velsn x B x = B
7 6 ralbii x A x B x A x = B
8 4 5 7 3bitr3i A = A = B x A x = B
9 3 8 bitrdi A A = B x A x = B