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

Metamath Proof Explorer

Theorem reuss

Description: Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999)

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

Step	Hyp	Ref	Expression
1		id	$⊢ φ \to φ$
2	1	rgenw	$⊢ \forall x \in A (φ \to φ)$
3		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 φ$
4	2 3	mpanl2	$⊢ (A \subseteq B \land (\exists x \in A φ \land \exists! x \in B φ)) \to \exists! x \in A φ$
5	4	3impb	$⊢ (A \subseteq B \land \exists x \in A φ \land \exists! x \in B φ) \to \exists! x \in A φ$