Metamath Proof Explorer

Theorem rmo0

Description: Vacuous restricted at-most-one quantifier is always true. (Contributed by AV, 3-Apr-2023)

Ref Expression
Assertion rmo0 
|- E* x e. (/) ph

Proof

Step Hyp Ref Expression
1 rex0 
 |-  -. E. x e. (/) ph
2 1 pm2.21i 
 |-  ( E. x e. (/) ph -> E! x e. (/) ph )
3 rmo5 
 |-  ( E* x e. (/) ph <-> ( E. x e. (/) ph -> E! x e. (/) ph ) )
4 2 3 mpbir 
 |-  E* x e. (/) ph