Theorem mosn

Description: "At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mosn	|- ( A = { B } -> E* x x e. A )

Proof

Step	Hyp	Ref	Expression
1		rmosn	|- E* x e. { B } T.
2		rmotru	|- ( E* x x e. { B } <-> E* x e. { B } T. )
3	1 2	mpbir	|- E* x x e. { B }
4		eleq2	|- ( A = { B } -> ( x e. A <-> x e. { B } ) )
5	4	mobidv	|- ( A = { B } -> ( E* x x e. A <-> E* x x e. { B } ) )
6	3 5	mpbiri	|- ( A = { B } -> E* x x e. A )