Metamath Proof Explorer


Theorem eqsnd

Description: Deduce that a set is a singleton. (Contributed by Thierry Arnoux, 10-May-2023) (Proof shortened by SN, 3-Jul-2025)

Ref Expression
Hypotheses eqsnd.1 φ x A x = B
eqsnd.2 φ B A
Assertion eqsnd φ A = B

Proof

Step Hyp Ref Expression
1 eqsnd.1 φ x A x = B
2 eqsnd.2 φ B A
3 1 ralrimiva φ x A x = B
4 2 ne0d φ A
5 eqsn A A = B x A x = B
6 4 5 syl φ A = B x A x = B
7 3 6 mpbird φ A = B