reuss2

Description: Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005)

		Ref	Expression
	Assertion	reuss2	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to \exists! x \in A φ$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
2		df-reu	$⊢ \exists! x \in B ψ \leftrightarrow \exists! x (x \in B \land ψ)$
3	1 2	anbi12i	$⊢ (\exists x \in A φ \land \exists! x \in B ψ) \leftrightarrow (\exists x (x \in A \land φ) \land \exists! x (x \in B \land ψ))$
4		df-ral	$⊢ \forall x \in A (φ \to ψ) \leftrightarrow \forall x (x \in A \to (φ \to ψ))$
5		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
6		pm3.2	$⊢ x \in B \to (ψ \to (x \in B \land ψ))$
7	6	imim2d	$⊢ x \in B \to ((φ \to ψ) \to (φ \to (x \in B \land ψ)))$
8	5 7	syl6	$⊢ A \subseteq B \to (x \in A \to ((φ \to ψ) \to (φ \to (x \in B \land ψ))))$
9	8	a2d	$⊢ A \subseteq B \to ((x \in A \to (φ \to ψ)) \to (x \in A \to (φ \to (x \in B \land ψ))))$
10	9	imp4a	$⊢ A \subseteq B \to ((x \in A \to (φ \to ψ)) \to ((x \in A \land φ) \to (x \in B \land ψ)))$
11	10	alimdv	$⊢ A \subseteq B \to (\forall x (x \in A \to (φ \to ψ)) \to \forall x ((x \in A \land φ) \to (x \in B \land ψ)))$
12	11	imp	$⊢ (A \subseteq B \land \forall x (x \in A \to (φ \to ψ))) \to \forall x ((x \in A \land φ) \to (x \in B \land ψ))$
13	4 12	sylan2b	$⊢ (A \subseteq B \land \forall x \in A (φ \to ψ)) \to \forall x ((x \in A \land φ) \to (x \in B \land ψ))$
14		euimmo	$⊢ \forall x ((x \in A \land φ) \to (x \in B \land ψ)) \to (\exists! x (x \in B \land ψ) \to \exists^{*} x (x \in A \land φ))$
15	13 14	syl	$⊢ (A \subseteq B \land \forall x \in A (φ \to ψ)) \to (\exists! x (x \in B \land ψ) \to \exists^{*} x (x \in A \land φ))$
16		df-eu	$⊢ \exists! x (x \in A \land φ) \leftrightarrow (\exists x (x \in A \land φ) \land \exists^{*} x (x \in A \land φ))$
17	16	simplbi2	$⊢ \exists x (x \in A \land φ) \to (\exists^{*} x (x \in A \land φ) \to \exists! x (x \in A \land φ))$
18	15 17	syl9	$⊢ (A \subseteq B \land \forall x \in A (φ \to ψ)) \to (\exists x (x \in A \land φ) \to (\exists! x (x \in B \land ψ) \to \exists! x (x \in A \land φ)))$
19	18	imp32	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x (x \in A \land φ) \land \exists! x (x \in B \land ψ))) \to \exists! x (x \in A \land φ)$
20		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
21	19 20	sylibr	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x (x \in A \land φ) \land \exists! x (x \in B \land ψ))) \to \exists! x \in A φ$
22	3 21	sylan2b	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to \exists! x \in A φ$

Metamath Proof Explorer

Theorem reuss2

Proof