Metamath Proof Explorer


Theorem reurex

Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999)

Ref Expression
Assertion reurex ∃!xAφxAφ

Proof

Step Hyp Ref Expression
1 reu5 ∃!xAφxAφ*xAφ
2 1 simplbi ∃!xAφxAφ