Theorem eqeuel

Description: A condition which implies the existence of a unique element of a class. (Contributed by AV, 4-Jan-2022)

	Ref	Expression
Assertion	eqeuel	|- ( ( A =/= (/) /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) -> E! x x e. A )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. x x e. A )
2	1	biimpi	|- ( A =/= (/) -> E. x x e. A )
3	2	anim1i	|- ( ( A =/= (/) /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) -> ( E. x x e. A /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) )
4		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
5	4	eu4	|- ( E! x x e. A <-> ( E. x x e. A /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) )
6	3 5	sylibr	|- ( ( A =/= (/) /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) -> E! x x e. A )