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

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 ⊢ ∀ x ∈ A φ → ψ → ∃! x ∈ A ψ → ∃* x ∈ A φ

Proof

Step Hyp Ref Expression
1 reurmo ⊢ ∃! x ∈ A ψ → ∃* x ∈ A ψ
2 rmoim ⊢ ∀ x ∈ A φ → ψ → ∃* x ∈ A ψ → ∃* x ∈ A φ
3 1 2 syl5 ⊢ ∀ x ∈ A φ → ψ → ∃! x ∈ A ψ → ∃* x ∈ A φ