Metamath Proof Explorer


Theorem eqsnd

Description: Deduce that a set is a singleton. (Contributed by Thierry Arnoux, 10-May-2023)

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 simpr φ x = B x = B
4 2 adantr φ x = B B A
5 3 4 eqeltrd φ x = B x A
6 1 5 impbida φ x A x = B
7 velsn x B x = B
8 6 7 bitr4di φ x A x B
9 8 eqrdv φ A = B