Metamath Proof Explorer


Theorem reuimrmo

Description: Restricted uniqueness implies restricted "at most one" through implication, analogous to euimmo . (Contributed by Alexander van der Vekens, 25-Jun-2017)

Ref Expression
Assertion reuimrmo xAφψ∃!xAψ*xAφ

Proof

Step Hyp Ref Expression
1 reurmo ∃!xAψ*xAψ
2 rmoim xAφψ*xAψ*xAφ
3 1 2 syl5 xAφψ∃!xAψ*xAφ