Metamath Proof Explorer

Theorem reu0

Description: Vacuous restricted uniqueness is always false. (Contributed by AV, 3-Apr-2023)

Ref Expression
Assertion reu0 
|- -. E! x e. (/) ph

Proof

Step Hyp Ref Expression
1 rex0 
 |-  -. E. x e. (/) ph
2 reurex 
 |-  ( E! x e. (/) ph -> E. x e. (/) ph )
3 1 2 mto 
 |-  -. E! x e. (/) ph