Metamath Proof Explorer

Theorem mosssn2

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024)

Ref Expression
Assertion mosssn2 
|- ( E* x x e. A <-> E. y A C_ { y } )

Proof

Step Hyp Ref Expression
1 19.45v 
 |-  ( E. y ( A = (/) \/ A = { y } ) <-> ( A = (/) \/ E. y A = { y } ) )
2 sssn 
 |-  ( A C_ { y } <-> ( A = (/) \/ A = { y } ) )
3 2 exbii 
 |-  ( E. y A C_ { y } <-> E. y ( A = (/) \/ A = { y } ) )
4 mo0sn 
 |-  ( E* x x e. A <-> ( A = (/) \/ E. y A = { y } ) )
5 1 3 4 3bitr4ri 
 |-  ( E* x x e. A <-> E. y A C_ { y } )