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

Metamath Proof Explorer

Theorem reupick

Description: Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999)

		Ref	Expression
	Assertion	reupick	$⊢ ((A \subseteq B \land (\exists x \in A φ \land \exists! x \in B φ)) \land φ) \to (x \in A \leftrightarrow x \in B)$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2	1	ad2antrr	$⊢ ((A \subseteq B \land (\exists x \in A φ \land \exists! x \in B φ)) \land φ) \to (x \in A \to x \in B)$
3		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
4		df-reu	$⊢ \exists! x \in B φ \leftrightarrow \exists! x (x \in B \land φ)$
5	3 4	anbi12i	$⊢ (\exists x \in A φ \land \exists! x \in B φ) \leftrightarrow (\exists x (x \in A \land φ) \land \exists! x (x \in B \land φ))$
6	1	ancrd	$⊢ A \subseteq B \to (x \in A \to (x \in B \land x \in A))$
7	6	anim1d	$⊢ A \subseteq B \to ((x \in A \land φ) \to ((x \in B \land x \in A) \land φ))$
8		an32	$⊢ ((x \in B \land x \in A) \land φ) \leftrightarrow ((x \in B \land φ) \land x \in A)$
9	7 8	imbitrdi	$⊢ A \subseteq B \to ((x \in A \land φ) \to ((x \in B \land φ) \land x \in A))$
10	9	eximdv	$⊢ A \subseteq B \to (\exists x (x \in A \land φ) \to \exists x ((x \in B \land φ) \land x \in A))$
11		eupick	$⊢ (\exists! x (x \in B \land φ) \land \exists x ((x \in B \land φ) \land x \in A)) \to ((x \in B \land φ) \to x \in A)$
12	11	ex	$⊢ \exists! x (x \in B \land φ) \to (\exists x ((x \in B \land φ) \land x \in A) \to ((x \in B \land φ) \to x \in A))$
13	10 12	syl9	$⊢ A \subseteq B \to (\exists! x (x \in B \land φ) \to (\exists x (x \in A \land φ) \to ((x \in B \land φ) \to x \in A)))$
14	13	com23	$⊢ A \subseteq B \to (\exists x (x \in A \land φ) \to (\exists! x (x \in B \land φ) \to ((x \in B \land φ) \to x \in A)))$
15	14	imp32	$⊢ (A \subseteq B \land (\exists x (x \in A \land φ) \land \exists! x (x \in B \land φ))) \to ((x \in B \land φ) \to x \in A)$
16	5 15	sylan2b	$⊢ (A \subseteq B \land (\exists x \in A φ \land \exists! x \in B φ)) \to ((x \in B \land φ) \to x \in A)$
17	16	expcomd	$⊢ (A \subseteq B \land (\exists x \in A φ \land \exists! x \in B φ)) \to (φ \to (x \in B \to x \in A))$
18	17	imp	$⊢ ((A \subseteq B \land (\exists x \in A φ \land \exists! x \in B φ)) \land φ) \to (x \in B \to x \in A)$
19	2 18	impbid	$⊢ ((A \subseteq B \land (\exists x \in A φ \land \exists! x \in B φ)) \land φ) \to (x \in A \leftrightarrow x \in B)$