Metamath Proof Explorer

Theorem rmosn

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

Ref Expression
Assertion rmosn 
|- E* x e. { A } ph

Proof

Step Hyp Ref Expression
1 idd 
 |-  ( A e. _V -> ( [. A / x ]. ph -> [. A / x ]. ph ) )
2 nfsbc1v 
 |-  F/ x [. A / x ]. ph
3 sbceq1a 
 |-  ( x = A -> ( ph <-> [. A / x ]. ph ) )
4 2 3 rexsngf 
 |-  ( A e. _V -> ( E. x e. { A } ph <-> [. A / x ]. ph ) )
5 2 3 reusngf 
 |-  ( A e. _V -> ( E! x e. { A } ph <-> [. A / x ]. ph ) )
6 1 4 5 3imtr4d 
 |-  ( A e. _V -> ( E. x e. { A } ph -> E! x e. { A } ph ) )
7 rmo5 
 |-  ( E* x e. { A } ph <-> ( E. x e. { A } ph -> E! x e. { A } ph ) )
8 6 7 sylibr 
 |-  ( A e. _V -> E* x e. { A } ph )
9 rmo0 
 |-  E* x e. (/) ph
10 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
11 rmoeq1 
 |-  ( { A } = (/) -> ( E* x e. { A } ph <-> E* x e. (/) ph ) )
12 10 11 sylbi 
 |-  ( -. A e. _V -> ( E* x e. { A } ph <-> E* x e. (/) ph ) )
13 9 12 mpbiri 
 |-  ( -. A e. _V -> E* x e. { A } ph )
14 8 13 pm2.61i 
 |-  E* x e. { A } ph