Metamath Proof Explorer

Theorem iotan0

Description: Representation of "the unique element such that ph " with a class expression A which is not the empty set (that means that "the unique element such that ph " exists). (Contributed by AV, 30-Jan-2024)

		Ref	Expression
	Hypothesis	iotan0.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	iotan0	$⊢ (A \in V \land A \neq \emptyset \land A = (ι x \| φ)) \to ψ$

Proof

Step	Hyp	Ref	Expression
1		iotan0.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		pm13.18	$⊢ (A = (ι x \| φ) \land A \neq \emptyset) \to (ι x \| φ) \neq \emptyset$
3	2	expcom	$⊢ A \neq \emptyset \to (A = (ι x \| φ) \to (ι x \| φ) \neq \emptyset)$
4		iotanul	$⊢ \neg \exists! x φ \to (ι x \| φ) = \emptyset$
5	4	necon1ai	$⊢ (ι x \| φ) \neq \emptyset \to \exists! x φ$
6	3 5	syl6	$⊢ A \neq \emptyset \to (A = (ι x \| φ) \to \exists! x φ)$
7	6	a1i	$⊢ A \in V \to (A \neq \emptyset \to (A = (ι x \| φ) \to \exists! x φ))$
8	7	3imp	$⊢ (A \in V \land A \neq \emptyset \land A = (ι x \| φ)) \to \exists! x φ$
9		eqcom	$⊢ A = (ι x \| φ) \leftrightarrow (ι x \| φ) = A$
10	1	iota2	$⊢ (A \in V \land \exists! x φ) \to (ψ \leftrightarrow (ι x \| φ) = A)$
11	10	biimprd	$⊢ (A \in V \land \exists! x φ) \to ((ι x \| φ) = A \to ψ)$
12	9 11	biimtrid	$⊢ (A \in V \land \exists! x φ) \to (A = (ι x \| φ) \to ψ)$
13	12	impancom	$⊢ (A \in V \land A = (ι x \| φ)) \to (\exists! x φ \to ψ)$
14	13	3adant2	$⊢ (A \in V \land A \neq \emptyset \land A = (ι x \| φ)) \to (\exists! x φ \to ψ)$
15	8 14	mpd	$⊢ (A \in V \land A \neq \emptyset \land A = (ι x \| φ)) \to ψ$