Metamath Proof Explorer


Theorem euimmo

Description: Existential uniqueness implies uniqueness through reverse implication. (Contributed by NM, 22-Apr-1995)

Ref Expression
Assertion euimmo xφψ∃!xψ*xφ

Proof

Step Hyp Ref Expression
1 eumo ∃!xψ*xψ
2 moim xφψ*xψ*xφ
3 1 2 syl5 xφψ∃!xψ*xφ