Metamath Proof Explorer

Theorem moel

Description: "At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018) Avoid ax-11 . (Revised by Wolf Lammen, 23-Nov-2024)

Ref Expression
Assertion moel 
|- ( E* x x e. A <-> A. x e. A A. y e. A x = y )

Proof

Step Hyp Ref Expression
1 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
2 1 mo4 
 |-  ( E* x x e. A <-> A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) )
3 r2al 
 |-  ( A. x e. A A. y e. A x = y <-> A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) )
4 2 3 bitr4i 
 |-  ( E* x x e. A <-> A. x e. A A. y e. A x = y )