Metamath Proof Explorer

Theorem mo0

Description: "At most one" element in an empty set. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion mo0 
|- ( A = (/) -> E* x x e. A )

Proof

Step Hyp Ref Expression
1 vsn 
 |-  { _V } = (/)
2 1 eqcomi 
 |-  (/) = { _V }
3 eqeq1 
 |-  ( A = (/) -> ( A = { _V } <-> (/) = { _V } ) )
4 2 3 mpbiri 
 |-  ( A = (/) -> A = { _V } )
5 mosn 
 |-  ( A = { _V } -> E* x x e. A )
6 4 5 syl 
 |-  ( A = (/) -> E* x x e. A )