iota2

Description: The unique element such that ph . (Contributed by Jeff Madsen, 1-Jun-2011) (Revised by Mario Carneiro, 23-Dec-2016)

		Ref	Expression
	Hypothesis	iota2.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	iota2	$⊢ (A \in B \land \exists! x φ) \to (ψ \leftrightarrow (ι x \| φ) = A)$

Step	Hyp	Ref	Expression
1		iota2.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		elex	$⊢ A \in B \to A \in V$
3		simpl	$⊢ (A \in V \land \exists! x φ) \to A \in V$
4		simpr	$⊢ (A \in V \land \exists! x φ) \to \exists! x φ$
5	1	adantl	$⊢ ((A \in V \land \exists! x φ) \land x = A) \to (φ \leftrightarrow ψ)$
6		nfv	$⊢ Ⅎ x A \in V$
7		nfeu1	$⊢ Ⅎ x \exists! x φ$
8	6 7	nfan	$⊢ Ⅎ x (A \in V \land \exists! x φ)$
9		nfvd	$⊢ (A \in V \land \exists! x φ) \to Ⅎ x ψ$
10		nfcvd	$⊢ (A \in V \land \exists! x φ) \to \underline{Ⅎ} x A$
11	3 4 5 8 9 10	iota2df	$⊢ (A \in V \land \exists! x φ) \to (ψ \leftrightarrow (ι x \| φ) = A)$
12	2 11	sylan	$⊢ (A \in B \land \exists! x φ) \to (ψ \leftrightarrow (ι x \| φ) = A)$

Metamath Proof Explorer