moriotass

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006) (Revised by NM, 16-Jun-2017)

		Ref	Expression
	Assertion	moriotass	$⊢ (A \subseteq B \land \exists x \in A φ \land \exists^{*} x \in B φ) \to (ι x \in A \| φ) = (ι x \in B \| φ)$

Step	Hyp	Ref	Expression
1		ssrexv	$⊢ A \subseteq B \to (\exists x \in A φ \to \exists x \in B φ)$
2	1	imp	$⊢ (A \subseteq B \land \exists x \in A φ) \to \exists x \in B φ$
3	2	3adant3	$⊢ (A \subseteq B \land \exists x \in A φ \land \exists^{*} x \in B φ) \to \exists x \in B φ$
4		simp3	$⊢ (A \subseteq B \land \exists x \in A φ \land \exists^{} x \in B φ) \to \exists^{} x \in B φ$
5		reu5	$⊢ \exists! x \in B φ \leftrightarrow (\exists x \in B φ \land \exists^{*} x \in B φ)$
6	3 4 5	sylanbrc	$⊢ (A \subseteq B \land \exists x \in A φ \land \exists^{*} x \in B φ) \to \exists! x \in B φ$
7		riotass	$⊢ (A \subseteq B \land \exists x \in A φ \land \exists! x \in B φ) \to (ι x \in A \| φ) = (ι x \in B \| φ)$
8	6 7	syld3an3	$⊢ (A \subseteq B \land \exists x \in A φ \land \exists^{*} x \in B φ) \to (ι x \in A \| φ) = (ι x \in B \| φ)$

Metamath Proof Explorer