This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rmoan

Description: Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017)

Ref Expression
Assertion rmoan 
|- ( E* x e. A ph -> E* x e. A ( ps /\ ph ) )

Proof

Step Hyp Ref Expression
1 moan 
 |-  ( E* x ( x e. A /\ ph ) -> E* x ( ps /\ ( x e. A /\ ph ) ) )
2 an12 
 |-  ( ( ps /\ ( x e. A /\ ph ) ) <-> ( x e. A /\ ( ps /\ ph ) ) )
3 2 mobii 
 |-  ( E* x ( ps /\ ( x e. A /\ ph ) ) <-> E* x ( x e. A /\ ( ps /\ ph ) ) )
4 1 3 sylib 
 |-  ( E* x ( x e. A /\ ph ) -> E* x ( x e. A /\ ( ps /\ ph ) ) )
5 df-rmo 
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
6 df-rmo 
 |-  ( E* x e. A ( ps /\ ph ) <-> E* x ( x e. A /\ ( ps /\ ph ) ) )
7 4 5 6 3imtr4i 
 |-  ( E* x e. A ph -> E* x e. A ( ps /\ ph ) )