reuhypd

Description: A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd . (Contributed by NM, 16-Jan-2012)

	Ref	Expression
Hypotheses	reuhypd.1	$⊢ (φ \land x \in C) \to B \in C$
	reuhypd.2	$⊢ (φ \land x \in C \land y \in C) \to (x = A \leftrightarrow y = B)$
Assertion	reuhypd	$⊢ (φ \land x \in C) \to \exists! y \in C x = A$

Step	Hyp	Ref	Expression
1		reuhypd.1	$⊢ (φ \land x \in C) \to B \in C$
2		reuhypd.2	$⊢ (φ \land x \in C \land y \in C) \to (x = A \leftrightarrow y = B)$
3	1	elexd	$⊢ (φ \land x \in C) \to B \in V$
4		eueq	$⊢ B \in V \leftrightarrow \exists! y y = B$
5	3 4	sylib	$⊢ (φ \land x \in C) \to \exists! y y = B$
6		eleq1	$⊢ y = B \to (y \in C \leftrightarrow B \in C)$
7	1 6	syl5ibrcom	$⊢ (φ \land x \in C) \to (y = B \to y \in C)$
8	7	pm4.71rd	$⊢ (φ \land x \in C) \to (y = B \leftrightarrow (y \in C \land y = B))$
9	2	3expa	$⊢ ((φ \land x \in C) \land y \in C) \to (x = A \leftrightarrow y = B)$
10	9	pm5.32da	$⊢ (φ \land x \in C) \to ((y \in C \land x = A) \leftrightarrow (y \in C \land y = B))$
11	8 10	bitr4d	$⊢ (φ \land x \in C) \to (y = B \leftrightarrow (y \in C \land x = A))$
12	11	eubidv	$⊢ (φ \land x \in C) \to (\exists! y y = B \leftrightarrow \exists! y (y \in C \land x = A))$
13	5 12	mpbid	$⊢ (φ \land x \in C) \to \exists! y (y \in C \land x = A)$
14		df-reu	$⊢ \exists! y \in C x = A \leftrightarrow \exists! y (y \in C \land x = A)$
15	13 14	sylibr	$⊢ (φ \land x \in C) \to \exists! y \in C x = A$

Metamath Proof Explorer