Theorem mosneq

Description: There exists at most one set whose singleton is equal to a given class. See also moeq . (Contributed by BJ, 24-Sep-2022)

	Ref	Expression
Assertion	mosneq	|- E* x { x } = A

Proof

Step	Hyp	Ref	Expression
1		eqtr3	|- ( ( { x } = A /\ { y } = A ) -> { x } = { y } )
2		vex	|- x e. _V
3	2	sneqr	|- ( { x } = { y } -> x = y )
4	1 3	syl	|- ( ( { x } = A /\ { y } = A ) -> x = y )
5	4	gen2	|- A. x A. y ( ( { x } = A /\ { y } = A ) -> x = y )
6		sneq	|- ( x = y -> { x } = { y } )
7	6	eqeq1d	|- ( x = y -> ( { x } = A <-> { y } = A ) )
8	7	mo4	|- ( E* x { x } = A <-> A. x A. y ( ( { x } = A /\ { y } = A ) -> x = y ) )
9	5 8	mpbir	|- E* x { x } = A