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	⊢ 𝐴 ∈ V
Assertion	eueqi	⊢ ∃! 𝑥 𝑥 = 𝐴

Proof

Step	Hyp	Ref	Expression
1		eueqi.1	⊢ 𝐴 ∈ V
2		eueq	⊢ ( 𝐴 ∈ V ↔ ∃! 𝑥 𝑥 = 𝐴 )
3	1 2	mpbi	⊢ ∃! 𝑥 𝑥 = 𝐴