Metamath Proof Explorer

Theorem eueqi

Description: There exists a unique set equal to a given set. Inference associated with euequ . See euequ in the case of a setvar. (Contributed by NM, 5-Apr-1995)

Ref Expression
Hypothesis eueqi.1 A V
Assertion eueqi ∃! x x = A


Step Hyp Ref Expression
1 eueqi.1 A V
2 eueq A V ∃! x x = A
3 1 2 mpbi ∃! x x = A