Metamath Proof Explorer

Theorem mosssn

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

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

Proof

Step Hyp Ref Expression
1 sssn 
 |-  ( A C_ { B } <-> ( A = (/) \/ A = { B } ) )
2 mo0 
 |-  ( A = (/) -> E* x x e. A )
3 mosn 
 |-  ( A = { B } -> E* x x e. A )
4 2 3 jaoi 
 |-  ( ( A = (/) \/ A = { B } ) -> E* x x e. A )
5 1 4 sylbi 
 |-  ( A C_ { B } -> E* x x e. A )