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

Metamath Proof Explorer

Theorem euequ

Description: There exists a unique set equal to a given set. Special case of eueqi proved using only predicate calculus. The proof needs y = z be free of x . This is ensured by having x and y be distinct. Alternately, a distinctor -. A. x x = y could have been used instead. See eueq and eueqi for classes. (Contributed by Stefan Allan, 4-Dec-2008) (Proof shortened by Wolf Lammen, 8-Sep-2019) Reduce axiom usage. (Revised by Wolf Lammen, 1-Mar-2023)

		Ref	Expression
	Assertion	euequ	$⊢ \exists! x x = y$

Proof

Step	Hyp	Ref	Expression
1		ax6ev	$⊢ \exists x x = y$
2		ax6ev	$⊢ \exists z z = y$
3		equeuclr	$⊢ z = y \to (x = y \to x = z)$
4	3	alrimiv	$⊢ z = y \to \forall x (x = y \to x = z)$
5	2 4	eximii	$⊢ \exists z \forall x (x = y \to x = z)$
6		eu3v	$⊢ \exists! x x = y \leftrightarrow (\exists x x = y \land \exists z \forall x (x = y \to x = z))$
7	1 5 6	mpbir2an	$⊢ \exists! x x = y$