Theorem eqsnd

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

	Ref	Expression
Hypotheses	eqsnd.1	|- ( ( ph /\ x e. A ) -> x = B )
	eqsnd.2	|- ( ph -> B e. A )
Assertion	eqsnd	|- ( ph -> A = { B } )

Proof

Step	Hyp	Ref	Expression
1		eqsnd.1	|- ( ( ph /\ x e. A ) -> x = B )
2		eqsnd.2	|- ( ph -> B e. A )
3		simpr	|- ( ( ph /\ x = B ) -> x = B )
4	2	adantr	|- ( ( ph /\ x = B ) -> B e. A )
5	3 4	eqeltrd	|- ( ( ph /\ x = B ) -> x e. A )
6	1 5	impbida	|- ( ph -> ( x e. A <-> x = B ) )
7		velsn	|- ( x e. { B } <-> x = B )
8	6 7	bitr4di	|- ( ph -> ( x e. A <-> x e. { B } ) )
9	8	eqrdv	|- ( ph -> A = { B } )