euelss

Description: Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ A \subseteq B \to A \subseteq B$
2		df-rex	$⊢ \exists x \in A ⊤ \leftrightarrow \exists x (x \in A \land ⊤)$
3		ancom	$⊢ (x \in A \land ⊤) \leftrightarrow (⊤ \land x \in A)$
4		truan	$⊢ (⊤ \land x \in A) \leftrightarrow x \in A$
5	3 4	bitri	$⊢ (x \in A \land ⊤) \leftrightarrow x \in A$
6	5	exbii	$⊢ \exists x (x \in A \land ⊤) \leftrightarrow \exists x x \in A$
7	2 6	sylbbr	$⊢ \exists x x \in A \to \exists x \in A ⊤$
8		df-reu	$⊢ \exists! x \in B ⊤ \leftrightarrow \exists! x (x \in B \land ⊤)$
9		ancom	$⊢ (x \in B \land ⊤) \leftrightarrow (⊤ \land x \in B)$
10		truan	$⊢ (⊤ \land x \in B) \leftrightarrow x \in B$
11	9 10	bitri	$⊢ (x \in B \land ⊤) \leftrightarrow x \in B$
12	11	eubii	$⊢ \exists! x (x \in B \land ⊤) \leftrightarrow \exists! x x \in B$
13	8 12	sylbbr	$⊢ \exists! x x \in B \to \exists! x \in B ⊤$
14		reuss	$⊢ (A \subseteq B \land \exists x \in A ⊤ \land \exists! x \in B ⊤) \to \exists! x \in A ⊤$
15	1 7 13 14	syl3an	$⊢ (A \subseteq B \land \exists x x \in A \land \exists! x x \in B) \to \exists! x \in A ⊤$
16		df-reu	$⊢ \exists! x \in A ⊤ \leftrightarrow \exists! x (x \in A \land ⊤)$
17	15 16	sylib	$⊢ (A \subseteq B \land \exists x x \in A \land \exists! x x \in B) \to \exists! x (x \in A \land ⊤)$
18		ancom	$⊢ (⊤ \land x \in A) \leftrightarrow (x \in A \land ⊤)$
19	4 18	bitr3i	$⊢ x \in A \leftrightarrow (x \in A \land ⊤)$
20	19	eubii	$⊢ \exists! x x \in A \leftrightarrow \exists! x (x \in A \land ⊤)$
21	17 20	sylibr	$⊢ (A \subseteq B \land \exists x x \in A \land \exists! x x \in B) \to \exists! x x \in A$

Metamath Proof Explorer

Theorem euelss

Proof